# Entrants' Sample Solutions

## CARINE 0.72

Paul Haroun, Monty Newborn
pharoun@cs.mcgill.ca
• Inferences are binary resolution and binary factoring.
• Input clauses are base clauses indicated by 'B' followed by an integer id.<
• Unit clauses are derived clauses. If the derivation is simply the unit clause itself then this unit clause is actually a base clause.
• Resolvents and factors are labeled with 'R' followed by the depth at which they are formed. Example: R3 means resolvent/factor generated at depth 3.

### CARINE Proof Format

```<derivation>    ::= <clause> ....... <clause id> | <inference><inference>*
<inference>     ::= <space><clause> ....... <clause id>
<space><clause> ....... <clause id>
<space><blank><resolvent_factor> ....... R<id>
[<clause id>:<literal id>, <clause id>:<literal id>]
<space>         ::= <blank>*
<blank>         ::= " "
<clause>        ::= <literal> <more literals>*
<literal>       ::= <sign><atom>
<more literals> ::= <or> <literal>
<sign>          ::= ~ | []
<atom>          ::= <proposition> | <predicate><arguments>
<or>            ::= |
<proposition>   ::= <identifier>
<predicate>     ::= <identifier>
<arguments>     ::= (<term><more terms>*)
<term>          ::= <constant> | <function> | <variable>
<more terms>    ::= ,<term>
<constant>      ::= <identifier>()
<function>      ::= <identifier><arguments>
<variable>      ::= <identifier>
<identifier>    ::= <legal character><legal character>*
legal character>::= A|B|C|D|E|F|G|H|I|J|K|L|M|N|O|P|Q|R|S|T|U|V|W|X|Y|Z|a|b|c|d|e|f|g|h|i|j|k|l|m|n|o|p|q|r|s|t|u|v|x|y|z|0|1|2|3|4|5|6|7|8|9|_
<clause id>     ::= B<id> | U<id> | R<id>
<id>            ::= <digit><digit>*
<digit>         ::= 0|1|2|3|4|5|6|7|8|9
<literal id>    :: = L<id>
<resolvent_factor>   ::= <clause> | "[]"
```
• <space> is a number of blanks indicating the search depth.
• Every clause in the proof is followed by its id for reference.
• Resolvents and factors have an id that is local to the derivation they are in.
• The empty clause is indicated by [].
• Each derivation is a linear resolution sequence.

### Sample Solution to Problem SYN075-1

```Base Clauses and Unit Clauses used in proof:
============================================

Base Clauses:
-------------
B0: ~equal(f(x0),x0) | big_f(h(x0,x1),f(x0)) | equal(h(x0,x1),x1)
B1: ~equal(x0,g(x1)) | big_f(x0,f(x1)) | equal(f(x1),x1)
B6: ~big_f(h(x0,x1),f(x0)) | ~equal(f(x0),x0) | ~equal(h(x0,x1),x1)
B7: equal(x0,x0)
B8: ~equal(x0,x1) | equal(x1,x0)
B9: ~big_f(x0,x1) | equal(x0,a())
B10: ~big_f(x0,x1) | equal(x1,b())
B15: ~equal(x0,x1) | ~equal(x1,x2) | equal(x0,x2)
B16: ~big_f(x0,x2) | ~equal(x0,x1) | big_f(x1,x2)
B18: ~equal(x0,a()) | ~equal(x1,b()) | big_f(x0,x1)

Unit Clauses:
--------------
U0: equal(x0,x0)
U71: equal(f(b()),b())
U72: ~big_f(h(b(),a()),f(b()))
U73: equal(b(),f(b()))
U90: big_f(a(),f(b()))
U138: ~equal(h(b(),a()),a())
U660: equal(h(b(),a()),a())

--------------- Start of Proof ---------------

Derivation of unit clause U0:
equal(x0,x0) ....... U0

Derivation of unit clause U71:
~equal(x0,g(x1)) | big_f(x0,f(x1)) | equal(f(x1),x1) ....... B1
~big_f(x0,x1) | equal(x1,b()) ....... B10
~equal(x0, g(x1)) | equal(f(x1), x1) | equal(f(x1), b()) ....... R1 [B1:L1, B10:L0]
~equal(x0, g(b())) | equal(f(b()), b()) ....... R2 [R1:L1, R1:L2]
equal(x0,x0) ....... U0
equal(f(b()), b()) ....... R3 [R2:L0, U0:L0]

Derivation of unit clause U72:
~big_f(h(x0,x1),f(x0)) | ~equal(f(x0),x0) | ~equal(h(x0,x1),x1) ....... B6
~big_f(x0,x1) | equal(x0,a()) ....... B9
~big_f(h(x0, a()), f(x0)) | ~equal(f(x0), x0) | ~big_f(h(x0, a()), x1) ....... R1 [B6:L2, B9:L1]
~equal(f(x0), x0) | ~big_f(h(x0, a()), f(x0)) ....... R2 [R1:L0, R1:L2]
equal(f(b()),b()) ....... U71
~big_f(h(b(), a()), f(b())) ....... R3 [R2:L0, U71:L0]

Derivation of unit clause U73:
equal(x0,x0) ....... B7
~equal(x0,x1) | ~equal(x1,x2) | equal(x0,x2) ....... B15
~equal(x0, x1) | equal(x0, x1) ....... R1 [B7:L0, B15:L0]
~equal(x0,x1) | equal(x1,x0) ....... B8
~equal(x0, x1) | equal(x1, x0) ....... R2 [R1:L1, B8:L0]
equal(f(b()),b()) ....... U71
equal(b(), f(b())) ....... R3 [R2:L0, U71:L0]

Derivation of unit clause U90:
equal(x0,x0) ....... B7
~equal(x0,a()) | ~equal(x1,b()) | big_f(x0,x1) ....... B18
~equal(x0, b()) | big_f(a(), x0) ....... R1 [B7:L0, B18:L0]
~equal(x0,x1) | equal(x1,x0) ....... B8
big_f(a(), x0) | ~equal(b(), x0) ....... R2 [R1:L0, B8:L1]
equal(b(),f(b())) ....... U73
big_f(a(), f(b())) ....... R3 [R2:L1, U73:L0]

Derivation of unit clause U138:
~equal(x0,x1) | equal(x1,x0) ....... B8
~big_f(x0,x2) | ~equal(x0,x1) | big_f(x1,x2) ....... B16
~equal(x0, x1) | ~big_f(x1, x2) | big_f(x0, x2) ....... R1 [B8:L1, B16:L1]
big_f(a(),f(b())) ....... U90
~equal(x0, a()) | big_f(x0, f(b())) ....... R2 [R1:L1, U90:L0]
~big_f(h(b(),a()),f(b())) ....... U72
~equal(h(b(), a()), a()) ....... R3 [R2:L1, U72:L0]

Derivation of unit clause U660:
~equal(f(x0),x0) | big_f(h(x0,x1),f(x0)) | equal(h(x0,x1),x1) ....... B0
~equal(x0,x1) | equal(x1,x0) ....... B8
~equal(f(x0), x0) | big_f(h(x0, x1), f(x0)) | equal(x1, h(x0, x1)) ....... R1 [B0:L2, B8:L0]
equal(f(b()),b()) ....... U71
big_f(h(b(), x0), f(b())) | equal(x0, h(b(), x0)) ....... R2 [R1:L0, U71:L0]
~equal(x0,x1) | equal(x1,x0) ....... B8
big_f(h(b(), x0), f(b())) | equal(h(b(), x0), x0) ....... R3 [R2:L1, B8:L0]
~big_f(h(b(),a()),f(b())) ....... U72
equal(h(b(), a()), a()) ....... R4 [R3:L0, U72:L0]

Derivation of the empty clause:
equal(h(b(),a()),a()) ....... U660
~equal(h(b(),a()),a()) ....... U138
[] ....... R1 [U660:L0, U138:L0]

--------------- End of Proof ---------------
```

## EP 0.8

Stephan Schulz
Technische Universität München, Germany, and RISC-Linz, Johannes Kepler Universität, Austria
schulz@informatik.tu-muenchen.de

Here is a list of all inferences:

er
Equality resolution: x!=a v x=x ==> a=a
pm
Paramodulation. Note that E considers all literals as equational, and thus also performs resolution by a combination of top-level paramodulation and clause normalization.
ef
Equality factoring (factor equations on one side only, move the remaining disequation into the precondition): x=a v b=c v x=d ==> a!=c v b=c vb=d
split
Clause splitting a la Vampire (non-deductive, but maintains unsatisfiability)
rw
Rewriting, each rw-expression corresponds to exacly one rewrite step with the named clause. This is also used for equational unfolding.
sr
Simplify-reflect: An (equational) version of unit-cutting. As as example, see this positive simplify-reflect step: [a=b], [f(a)!=f(b)] => [].
ar
AC-resolution: Delete literals that are trivial modulo the AC-theory induced by the named clauses
cn
Clause normalize, delete trivial and repeated literals

The first proof uses all but "ef", although it uses some in fairly trivial ways. Note that clause normalization is inherently performed after all inferences but rewriting. The second is the required proof for SYN075-1, and contains an example for "ef".

### ALL_RULES

```# Problem is unsatisfiable, constructing proof object
# TSTP exit status: Unsatisfiable
# Proof object starts here.
1 : [++equal(f(X1,X2), f(X2,X1))] : initial
2 : [++equal(f(X1,f(X2,X3)), f(f(X1,X2),X3))] : initial
3 : [++equal(g(X1,X2), g(X2,X1))] : initial
4 : [--equal(f(f(X1,X2),f(X3,g(X4,X5))), f(f(g(X4,X5),X3),f(X2,X1))),--equal(k(X1,X1), k(a,b))] : initial
5 : [++equal(b, c),--equal(X1, X2),--equal(X3, X4),--equal(c, d)] : initial
6 : [++equal(a, b),++equal(a, c)] : initial
7 : [++equal(i(X1), i(X2))] : initial
8 : [++equal(c, d),--equal(h(i(a)), h(i(e)))] : initial
13 : [--equal(k(a,b), k(X1,X1))] : ar(4,1,3,2)
23 : [++equal(c, b),++epred1_0,--equal(d, c),--equal(X3, X4)] : split(5)
24 : [++epred2_0,--equal(X1, X2)] : split(5)
25 : [--epred2_0,--epred1_0] : split(5)
26 : [++epred2_0] : er(24)
27 : [--\$true,--epred1_0] : rw(25,26)
28 : [++equal(c, b),++epred1_0,--equal(d, c)] : er(23)
29 : [++equal(c, b),--equal(d, c)] : sr(28,27)
30 : [++equal(d, c)] : sr(8,7)
31 : [++equal(c, b),--equal(c, c)] : rw(29,30)
32 : [++equal(c, b)] : cn(31)
34 : [++equal(b, a)] : pm(6,32)
35 : [--equal(k(b,b), k(X1,X1))] : rw(13,34)
120 : [] : er(35)
121 : [] : 120 : "proof"
# Proof object ends here.
```

### Sample solution for SYN075-1

```# Problem is unsatisfiable, constructing proof object
# TSTP exit status: Unsatisfiable
# Proof object starts here.
1 : [++equal(X1, a),--big_f(X1,X2)] : initial
3 : [++big_f(X1,X2),--equal(X1, a),--equal(X2, b)] : initial
4 : [++equal(f(X2), X2),--big_f(X1,f(X2)),--equal(X1, g(X2))] : initial
6 : [++big_f(X1,f(X2)),++equal(f(X2), X2),--equal(X1, g(X2))] : initial
9 : [++big_f(h(X1,X2),f(X1)),++equal(h(X1,X2), X2),--equal(f(X1), X1)] : initial
10 : [--equal(f(X1), X1),--equal(h(X1,X2), X2),--big_f(h(X1,X2),f(X1))] : initial
18 : [++equal(f(X2), X2),--equal(g(X2), X1)] : pm(4,6)
19 : [++equal(f(X1), X1)] : er(18)
24 : [--equal(X1, X1),--equal(h(X1,X2), X2),--big_f(h(X1,X2),f(X1))] : rw(10,19)
25 : [--equal(X1, X1),--equal(h(X1,X2), X2),--big_f(h(X1,X2),X1)] : rw(24,19)
26 : [--equal(h(X1,X2), X2),--big_f(h(X1,X2),X1)] : cn(25)
27 : [++equal(h(X1,X2), X2),++big_f(h(X1,X2),X1),--equal(f(X1), X1)] : rw(9,19)
28 : [++equal(h(X1,X2), X2),++big_f(h(X1,X2),X1),--equal(X1, X1)] : rw(27,19)
29 : [++equal(h(X1,X2), X2),++big_f(h(X1,X2),X1)] : cn(28)
30 : [++equal(a, h(X1,X2)),++equal(h(X1,X2), X2)] : pm(1,29)
36 : [++equal(h(X1,X2), X2),--equal(a, X2)] : ef(30)
46 : [--big_f(X2,X1),--equal(h(X1,X2), X2),--equal(a, X2)] : pm(26,36)
56 : [--big_f(X2,X1),--equal(a, X2)] : pm(46,36)
63 : [--equal(a, X1),--equal(b, X2)] : pm(56,3)
94 : [--equal(b, X1)] : er(63)
103 : [] : er(94)
104 : [] : 103 : "proof"
# Proof object ends here.
```

## Gandalf c-2.6

Tanel Tammet
Tallinn Technical University, Estonia
tammet@cc.ttu.ee

### Sample Refutation

```START OF PROOF
12 [] equal(X,X).
13 [] equal(X,a) | -big_f(X,Y).
15 [] -equal(Y,b) | -equal(X,a) | big_f(X,Y).
17 [] big_f(h(X,Y),f(X)) | equal(h(X,Y),Y) | -equal(f(X),X).
20 [] -equal(X,g(Y)) | big_f(X,f(Y)) | equal(f(Y),Y).
22 [] -big_f(X,f(Y)) | -equal(X,g(Y)) | equal(f(Y),Y).
27 [] -big_f(h(X,Y),f(X)) | -equal(h(X,Y),Y) | -equal(f(X),X).
30 [hyper:20,12] big_f(g(X),f(X)) | equal(f(X),X).
32 [hyper:22,12,binarycut:30] equal(f(X),X).
35 [hyper:15,12,12] big_f(a,b).
38 [hyper:17,32,demod:32] big_f(h(X,Y),X) | equal(h(X,Y),Y).
82 [hyper:13,38,factor] equal(h(X,a),a).
END OF PROOF
```

### Sample Refutation with Splitting

```Gandalf v. c-2.6 beta starting to prove: /tmp/GandalfTemp4115

prove-all-passes started

detected problem class: peq

strategies selected:
(hyper 30 #f 12 5)
(binary-unit 12 #f)
(binary-unit-uniteq 12 #f)
(binary-posweight-kb-big-order 60 #f 12 5)
(binary-posweight-lex-big-order 30 #f 12 5)
(binary 30 #t)
(binary-posweight-kb-big-order 156 #f)
(binary-posweight-lex-big-order 102 #f)
(binary-posweight-firstpref-order 60 #f)
(binary-order 30 #f)
(binary-posweight-kb-small-order 48 #f)
(binary-posweight-lex-small-order 30 #f)

SOS clause
-equal(multiply(inverse(a1),a1),multiply(inverse(b1),b1)) | -equal(multiply(multiply(inverse(b2),b2),a2),a2) | -equal(multiply(multiply(a3,b3),c3),multiply(a3,multiply(b3,c3))).
was split for some strategies as:
-equal(multiply(inverse(a1),a1),multiply(inverse(b1),b1)).
-equal(multiply(multiply(inverse(b2),b2),a2),a2).
-equal(multiply(multiply(a3,b3),c3),multiply(a3,multiply(b3,c3))).

Starting a split proof attempt with 3 components.

Split component 1 started.

START OF PROOFPART
Making new sos for split:
Original clause to be split:
-equal(multiply(inverse(a1),a1),multiply(inverse(b1),b1)) | -equal(multiply(multiply(inverse(b2),b2),a2),a2) | -equal(multiply(multiply(a3,b3),c3),multiply(a3,multiply(b3,c3))).
Split part used next: -equal(multiply(inverse(a1),a1),multiply(inverse(b1),b1)).
END OF PROOFPART
**** EMPTY CLAUSE DERIVED ****

timer checkpoints: c(3,40,2,6,0,2,13,50,5,16,0,5,9528,4,711,9663,5,906,9663,1,906,9663,50,908,9663,40,908,9666,0,908,10991,3,1113,12378,4,1211,14866,5,1393,14866,1,1393,14866,50,1394,14866,40,1394,14869,0,1394,17337,3,1656,17892,4,1697,19772,5,1795,19784,1,1795,19784,50,1796,19784,40,1796,19787,0,1796,19794,50,1798,19797,0,1798,28123,3,2840,32590,4,3312,37306,5,3747,37308,1,3747,37308,50,3750,37308,40,3750,37311,0,3750,37318,50,3752,37321,0,3752,44100,3,4227,51250,4,4433,55491,5,4653,55493,1,4653,55493,50,4656,55493,40,4656,55496,0,4656,55497,50,4656,55497,40,4656,55500,0,4656,81692,3,7398,89382,4,8908,98454,5,9857,98462,1,9857,98462,50,9860,98462,40,9860,98465,0,9860,118207,3,12472,118207,4,12472,126466,5,13261,126489,1,13263,126489,50,13266,126489,40,13266,126492,0,13266,136384,3,14336,141920,4,14775,148496,5,15470,148507,1,15470,148507,50,15473,148507,40,15473,148510,0,15473,155256,3,15983,161622,4,16226,162526,5,16474,162526,1,16474,162526,50,16476,162526,40,16476,162529,0,16476,174482,3,17313,178673,4,17695,188717,5,18077,188719,1,18077,188719,50,18079,188719,40,18079,188722,0,18079,194033,3,18627,200190,4,18838,206431,5,19080,206431,1,19080,206431,50,19083,206431,40,19083,206431,40,19083,206434,0,19083,206440,50,19085,206443,0,19085)

START OF PROOF
206442 [] equal(inverse(multiply(inverse(multiply(X,inverse(multiply(inverse(Y),inverse(multiply(Z,inverse(multiply(inverse(Z),Z)))))))),multiply(X,Z))),Y).
206443 [] -equal(multiply(inverse(a1),a1),multiply(inverse(b1),b1)).
206444 [para:206442.1.1,206442.1.1.1.1.1.2.1.1] equal(inverse(multiply(inverse(multiply(X,inverse(multiply(Y,inverse(multiply(Z,inverse(multiply(inverse(Z),Z)))))))),multiply(X,Z))),multiply(inverse(multiply(U,inverse(multiply(inverse(Y),inverse(multiply(V,inverse(multiply(inverse(V),V)))))))),multiply(U,V))).
206445 [para:206444.1.1,206442.1.1] equal(multiply(inverse(multiply(X,inverse(multiply(inverse(inverse(Y)),inverse(multiply(Z,inverse(multiply(inverse(Z),Z)))))))),multiply(X,Z)),Y).
206453 [para:206445.1.1,206445.1.1.2] equal(multiply(inverse(multiply(inverse(multiply(X,inverse(multiply(inverse(inverse(Y)),inverse(multiply(Z,inverse(multiply(inverse(Z),Z)))))))),inverse(multiply(inverse(inverse(U)),inverse(multiply(multiply(X,Z),inverse(multiply(inverse(multiply(X,Z)),multiply(X,Z))))))))),Y),U).
206466 [para:206453.1.1,206442.1.1.1.1.1.2.1] equal(inverse(multiply(inverse(multiply(X,inverse(Y))),multiply(X,Z))),multiply(inverse(multiply(U,inverse(multiply(inverse(inverse(inverse(multiply(Z,inverse(multiply(inverse(Z),Z)))))),inverse(multiply(V,inverse(multiply(inverse(V),V)))))))),inverse(multiply(inverse(inverse(Y)),inverse(multiply(multiply(U,V),inverse(multiply(inverse(multiply(U,V)),multiply(U,V))))))))).
206473 [para:206466.1.2,206444.1.2.1.1,demod:206445,206442] equal(X,multiply(inverse(inverse(multiply(inverse(multiply(Y,inverse(X))),multiply(Y,Z)))),inverse(multiply(Z,inverse(multiply(inverse(Z),Z)))))).
206481 [para:206466.1.2,206466.1.2] equal(inverse(multiply(inverse(multiply(X,inverse(Y))),multiply(X,Z))),inverse(multiply(inverse(multiply(U,inverse(Y))),multiply(U,Z)))).
206482 [para:206481.1.1,206442.1.1.1.1.1.2.1.1,demod:206442] equal(multiply(inverse(multiply(X,inverse(Y))),multiply(X,Z)),multiply(inverse(multiply(U,inverse(Y))),multiply(U,Z))).
206506 [para:206442.1.1,206482.1.1.1.1.2,demod:206442] equal(multiply(inverse(multiply(X,Y)),multiply(X,Z)),multiply(inverse(multiply(U,Y)),multiply(U,Z))).
206537 [para:206506.1.1,206442.1.1.1.1.1.2.1.2.1.2.1] equal(inverse(multiply(inverse(multiply(X,inverse(multiply(inverse(Y),inverse(multiply(multiply(Z,U),inverse(multiply(inverse(multiply(V,U)),multiply(V,U))))))))),multiply(X,multiply(Z,U)))),Y).
206575 [para:206506.1.1,206453.1.1.1.1.2.1.2.1.2.1] equal(multiply(inverse(multiply(inverse(multiply(X,inverse(multiply(inverse(inverse(Y)),inverse(multiply(Z,inverse(multiply(inverse(Z),Z)))))))),inverse(multiply(inverse(inverse(U)),inverse(multiply(multiply(X,Z),inverse(multiply(inverse(multiply(V,Z)),multiply(V,Z))))))))),Y),U).
207691 [para:206453.1.1,206537.1.1.1.1.1.2.1.2.1.1,demod:206575] equal(inverse(multiply(inverse(multiply(X,inverse(multiply(inverse(Y),inverse(multiply(Z,inverse(multiply(inverse(multiply(U,V)),multiply(U,V))))))))),multiply(X,Z))),Y).
207713 [para:206445.1.1,207691.1.1.1.1.1.2.1.2.1.2.1.1.1,demod:206445] equal(inverse(multiply(inverse(multiply(X,inverse(multiply(inverse(Y),inverse(multiply(Z,inverse(multiply(inverse(U),U)))))))),multiply(X,Z))),Y).
207760 [para:207713.1.1,206473.1.2.1.1] equal(multiply(inverse(X),inverse(multiply(Y,inverse(multiply(inverse(Z),Z))))),multiply(inverse(X),inverse(multiply(Y,inverse(multiply(inverse(Y),Y)))))).
207856 [para:207760.1.2,206473.1.2] equal(X,multiply(inverse(inverse(multiply(inverse(multiply(Y,inverse(X))),multiply(Y,Z)))),inverse(multiply(Z,inverse(multiply(inverse(U),U)))))).
207857 [para:207760.1.1,206473.1.2.1.1.1.1.1,demod:207856] equal(multiply(X,inverse(multiply(inverse(Y),Y))),multiply(X,inverse(multiply(inverse(X),X)))).
END OF PROOF

Proof found by the following strategy:

using hyperresolution
not using sos strategy
using positive unit paramodulation strategy
using dynamic demodulation
using ordered paramodulation
using kb ordering for equality
preferring bigger arities for lex ordering
clause length limited to 5
clause depth limited to 13
seconds given: 12

Split component 2 started.

START OF PROOFPART
Making new sos for split:
Original clause to be split:
-equal(multiply(inverse(a1),a1),multiply(inverse(b1),b1)) | -equal(multiply(multiply(inverse(b2),b2),a2),a2) | -equal(multiply(multiply(a3,b3),c3),multiply(a3,multiply(b3,c3))).
Split part used next: -equal(multiply(multiply(inverse(b2),b2),a2),a2).
END OF PROOFPART
using hyperresolution
not using sos strategy
using positive unit paramodulation strategy
using dynamic demodulation
using ordered paramodulation
using kb ordering for equality
preferring bigger arities for lex ordering
clause length limited to 5
clause depth limited to 12
seconds given: 12

proof attempt stopped: sos exhausted

using hyperresolution
not using sos strategy
using positive unit paramodulation strategy
using dynamic demodulation
using ordered paramodulation
using kb ordering for equality
preferring bigger arities for lex ordering
clause length limited to 5
clause depth limited to 13
seconds given: 12

proof attempt stopped: time limit

using binary resolution
not using sos strategy
using unit strategy
using dynamic demodulation
using ordered paramodulation
using kb ordering for equality
preferring bigger arities for lex ordering
using clause demodulation
seconds given: 4

proof attempt stopped: time limit

using binary resolution
not using sos strategy
using unit paramodulation strategy
using unit strategy
using dynamic demodulation
using ordered paramodulation
using kb ordering for equality
preferring bigger arities for lex ordering
using clause demodulation
seconds given: 4

proof attempt stopped: time limit

using binary resolution
using first neg lit preferred strategy
not using sos strategy
using dynamic demodulation
using ordered paramodulation
using kb ordering for equality
preferring bigger arities for lex ordering
using clause demodulation
clause length limited to 5
clause depth limited to 12
seconds given: 26

proof attempt stopped: sos exhausted

using binary resolution
using first neg lit preferred strategy
not using sos strategy
using dynamic demodulation
using ordered paramodulation
using kb ordering for equality
preferring bigger arities for lex ordering
using clause demodulation
clause length limited to 5
clause depth limited to 13
seconds given: 26

proof attempt stopped: time limit

using binary resolution
using first neg lit preferred strategy
not using sos strategy
using dynamic demodulation
using ordered paramodulation
using lex ordering for equality
preferring bigger arities for lex ordering
using clause demodulation
clause length limited to 5
clause depth limited to 12
seconds given: 12

proof attempt stopped: sos exhausted

using binary resolution
using first neg lit preferred strategy
not using sos strategy
using dynamic demodulation
using ordered paramodulation
using lex ordering for equality
preferring bigger arities for lex ordering
using clause demodulation
clause length limited to 5
clause depth limited to 13
seconds given: 12

proof attempt stopped: time limit

using binary resolution
using sos strategy
using dynamic demodulation
using ordered paramodulation
using kb ordering for equality
preferring bigger arities for lex ordering
using clause demodulation
seconds given: 12

proof attempt stopped: sos exhausted

using binary resolution
using first neg lit preferred strategy
not using sos strategy
using dynamic demodulation
using ordered paramodulation
using kb ordering for equality
preferring bigger arities for lex ordering
using clause demodulation
seconds given: 68

proof attempt stopped: time limit

using binary resolution
using first neg lit preferred strategy
not using sos strategy
using dynamic demodulation
using ordered paramodulation
using lex ordering for equality
preferring bigger arities for lex ordering
using clause demodulation
seconds given: 44

proof attempt stopped: time limit

using binary resolution
using first neg lit preferred strategy
not using sos strategy
using dynamic demodulation
using ordered paramodulation
using first arg depth ordering for equality
preferring bigger arities for lex ordering
using clause demodulation
seconds given: 26

proof attempt stopped: time limit

using binary resolution
using term-depth-order strategy
not using sos strategy
using dynamic demodulation
using ordered paramodulation
using kb ordering for equality
preferring bigger arities for lex ordering
using clause demodulation
seconds given: 12

proof attempt stopped: time limit

using binary resolution
using first neg lit preferred strategy
not using sos strategy
using dynamic demodulation
using ordered paramodulation
using kb ordering for equality
preferring smaller arities for lex ordering
using clause demodulation
seconds given: 20

proof attempt stopped: time limit

using binary resolution
using first neg lit preferred strategy
not using sos strategy
using dynamic demodulation
using ordered paramodulation
using lex ordering for equality
preferring smaller arities for lex ordering
using clause demodulation
seconds given: 130

**** EMPTY CLAUSE DERIVED ****

timer checkpoints: c(3,40,2,6,0,2,13,50,5,16,0,5,9528,4,711,9663,5,906,9663,1,906,9663,50,908,9663,40,908,9666,0,908,10991,3,1113,12378,4,1211,14866,5,1393,14866,1,1393,14866,50,1394,14866,40,1394,14869,0,1394,17337,3,1656,17892,4,1697,19772,5,1795,19784,1,1795,19784,50,1796,19784,40,1796,19787,0,1796,19794,50,1798,19797,0,1798,28123,3,2840,32590,4,3312,37306,5,3747,37308,1,3747,37308,50,3750,37308,40,3750,37311,0,3750,37318,50,3752,37321,0,3752,44100,3,4227,51250,4,4433,55491,5,4653,55493,1,4653,55493,50,4656,55493,40,4656,55496,0,4656,55497,50,4656,55497,40,4656,55500,0,4656,81692,3,7398,89382,4,8908,98454,5,9857,98462,1,9857,98462,50,9860,98462,40,9860,98465,0,9860,118207,3,12472,118207,4,12472,126466,5,13261,126489,1,13263,126489,50,13266,126489,40,13266,126492,0,13266,136384,3,14336,141920,4,14775,148496,5,15470,148507,1,15470,148507,50,15473,148507,40,15473,148510,0,15473,155256,3,15983,161622,4,16226,162526,5,16474,162526,1,16474,162526,50,16476,162526,40,16476,162529,0,16476,174482,3,17313,178673,4,17695,188717,5,18077,188719,1,18077,188719,50,18079,188719,40,18079,188722,0,18079,194033,3,18627,200190,4,18838,206431,5,19080,206431,1,19080,206431,50,19083,206431,40,19083,206431,40,19083,206434,0,19083,206440,50,19085,206443,0,19085,208105,50,19282,208105,30,19282,208105,40,19282,208108,0,19282,208114,50,19284,208117,0,19284,217556,4,20130,218132,5,20385,218134,1,20386,218134,50,20386,218134,40,20386,218137,0,20386,220622,3,20602,221096,5,20861,221100,1,20861,221100,50,20862,221100,40,20862,221103,0,20862,223588,3,21097,224339,4,21169,225743,5,21263,225752,1,21263,225752,50,21263,225752,40,21263,225755,0,21263,225761,50,21265,225764,0,21497,234777,3,22756,239295,4,23428,242373,5,23998,242376,1,23998,242376,50,23998,242376,40,23998,242379,0,23999,242385,50,24001,242388,0,24001,245322,3,24559,247872,4,24849,250412,5,25102,250422,1,25102,250422,50,25103,250422,40,25103,250425,0,25103,250425,50,25103,250425,40,25103,250428,0,25103,270586,3,28515,277106,4,30352,281446,5,31904,281446,1,31904,281446,50,31904,281446,40,31904,281449,0,31904,302407,3,34111,308900,4,35270,315476,5,36305,315476,1,36305,315476,50,36306,315476,40,36306,315479,0,36306,325270,3,37607,328904,4,38271,331251,5,38908,331259,1,38908,331259,50,38908,331259,40,38908,331262,0,38908,340711,3,39530,341624,4,39820,344416,5,40109,344426,1,40109,344426,50,40110,344426,40,40110,344429,0,40110,354859,3,41131,359394,4,41614,362901,5,42208,362908,1,42209,362908,50,42210,362908,40,42210,362911,0,42210)

START OF PROOF
13810 [?] ?
13838 [?] ?
14020 [para:13810.1.1,13838.1.1.1.1] equal(inverse(inverse(inverse(inverse(inverse(multiply(inverse(X),X)))))),inverse(multiply(inverse(Y),Y))).
14873 [?] ?
18935 [?] ?
19248 [para:14873.1.1,18935.1.2.1.1,demod:14873] equal(multiply(inverse(X),X),multiply(inverse(Y),Y)).
70137 [?] ?
71493 [?] ?
97873 [para:70137.1.1,71493.1.1.1.2.1.2] equal(inverse(multiply(multiply(inverse(X),X),inverse(multiply(Y,multiply(inverse(Z),Z))))),Y).
105933 [?] ?
106140 [?] ?
106412 [para:106140.1.2,105933.1.1.1] equal(multiply(multiply(inverse(X),X),inverse(multiply(inverse(Y),Y))),inverse(multiply(inverse(Z),Z))).
152443 [?] ?
155821 [?] ?
155996 [para:152443.1.1,155821.1.1.1.1] equal(inverse(multiply(inverse(multiply(inverse(X),X)),multiply(inverse(Y),Y))),multiply(inverse(Z),Z)).
362910 [] equal(inverse(multiply(inverse(multiply(X,inverse(multiply(inverse(Y),inverse(multiply(Z,inverse(multiply(inverse(Z),Z)))))))),multiply(X,Z))),Y).
362911 [] -equal(multiply(multiply(inverse(b2),b2),a2),a2).
362912 [para:19248.1.1,362911.1.1.1] -equal(multiply(multiply(inverse(X),X),a2),a2).
362913 [para:19248.1.1,19248.1.1] equal(multiply(inverse(X),X),multiply(inverse(Y),Y)).
362929 [para:362913.1.1,14020.1.1.1.1.1.1.1] equal(inverse(inverse(inverse(inverse(inverse(multiply(inverse(X),X)))))),inverse(multiply(inverse(Y),Y))).
362933 [para:362913.1.1,97873.1.1.1.1] equal(inverse(multiply(multiply(inverse(X),X),inverse(multiply(Y,multiply(inverse(Z),Z))))),Y).
362935 [para:362929.1.1,362929.1.1] equal(inverse(multiply(inverse(X),X)),inverse(multiply(inverse(Y),Y))).
362943 [para:362935.1.1,362913.1.1.1] equal(multiply(inverse(multiply(inverse(X),X)),multiply(inverse(Y),Y)),multiply(inverse(Z),Z)).
363069 [para:106412.1.1,362933.1.1.1] equal(inverse(inverse(multiply(inverse(X),X))),inverse(multiply(inverse(Y),Y))).
363136 [para:363069.1.2,362912.1.1.1.1] -equal(multiply(multiply(inverse(inverse(multiply(inverse(X),X))),multiply(inverse(Y),Y)),a2),a2).
364157 [para:362913.1.1,155996.1.1.1] equal(inverse(multiply(inverse(X),X)),multiply(inverse(Y),Y)).
364188 [para:155996.1.1,362943.1.1.1] equal(multiply(multiply(inverse(X),X),multiply(inverse(Y),Y)),multiply(inverse(Z),Z)).
364207 [para:155996.1.1,363069.1.2] equal(inverse(inverse(multiply(inverse(X),X))),multiply(inverse(Y),Y)).
364284 [para:155996.1.2,363136.1.1.1.2] -equal(multiply(multiply(inverse(inverse(multiply(inverse(X),X))),inverse(multiply(inverse(multiply(inverse(Y),Y)),multiply(inverse(Z),Z)))),a2),a2).
364302 [para:364157.1.2,362933.1.1.1.2.1.2] equal(inverse(multiply(multiply(inverse(X),X),inverse(multiply(Y,inverse(multiply(inverse(Z),Z)))))),Y).
364364 [para:364157.1.1,364157.1.1.1.1] equal(inverse(multiply(multiply(inverse(X),X),multiply(inverse(Y),Y))),multiply(inverse(Z),Z)).
364365 [para:364157.1.1,364157.1.2.1] equal(inverse(multiply(inverse(X),X)),multiply(multiply(inverse(Y),Y),multiply(inverse(Z),Z))).
364436 [para:364207.1.1,362913.1.1.1] equal(multiply(multiply(inverse(X),X),inverse(multiply(inverse(Y),Y))),multiply(inverse(Z),Z)).
365858 [para:364364.1.2,362933.1.1.1.2.1.2] equal(inverse(multiply(multiply(inverse(X),X),inverse(multiply(Y,inverse(multiply(multiply(inverse(Z),Z),multiply(inverse(U),U))))))),Y).
369913 [para:364188.1.1,362910.1.1.1.2,demod:364302,362933] equal(inverse(multiply(inverse(X),multiply(inverse(Y),Y))),X).
369939 [para:364365.1.2,362910.1.1.1.2,demod:365858,369913] equal(inverse(multiply(inverse(X),inverse(multiply(inverse(Y),Y)))),X).
END OF PROOF

Proof found by the following strategy:

using binary resolution
using first neg lit preferred strategy
not using sos strategy
using dynamic demodulation
using ordered paramodulation
using lex ordering for equality
preferring smaller arities for lex ordering
using clause demodulation
seconds given: 130

Split component 3 started.

START OF PROOFPART
Making new sos for split:
Original clause to be split:
-equal(multiply(inverse(a1),a1),multiply(inverse(b1),b1)) | -equal(multiply(multiply(inverse(b2),b2),a2),a2) | -equal(multiply(multiply(a3,b3),c3),multiply(a3,multiply(b3,c3))).
Split part used next: -equal(multiply(multiply(a3,b3),c3),multiply(a3,multiply(b3,c3))).
END OF PROOFPART
using hyperresolution
not using sos strategy
using positive unit paramodulation strategy
using dynamic demodulation
using ordered paramodulation
using kb ordering for equality
preferring bigger arities for lex ordering
clause length limited to 5
clause depth limited to 12
seconds given: 12

proof attempt stopped: sos exhausted

using hyperresolution
not using sos strategy
using positive unit paramodulation strategy
using dynamic demodulation
using ordered paramodulation
using kb ordering for equality
preferring bigger arities for lex ordering
clause length limited to 5
clause depth limited to 13
seconds given: 12

proof attempt stopped: sos exhausted

using binary resolution
not using sos strategy
using unit strategy
using dynamic demodulation
using ordered paramodulation
using kb ordering for equality
preferring bigger arities for lex ordering
using clause demodulation
seconds given: 4

proof attempt stopped: time limit

using binary resolution
not using sos strategy
using unit paramodulation strategy
using unit strategy
using dynamic demodulation
using ordered paramodulation
using kb ordering for equality
preferring bigger arities for lex ordering
using clause demodulation
seconds given: 4

proof attempt stopped: time limit

using binary resolution
using first neg lit preferred strategy
not using sos strategy
using dynamic demodulation
using ordered paramodulation
using kb ordering for equality
preferring bigger arities for lex ordering
using clause demodulation
clause length limited to 5
clause depth limited to 12
seconds given: 26

proof attempt stopped: sos exhausted

using binary resolution
using first neg lit preferred strategy
not using sos strategy
using dynamic demodulation
using ordered paramodulation
using kb ordering for equality
preferring bigger arities for lex ordering
using clause demodulation
clause length limited to 5
clause depth limited to 13
seconds given: 26

proof attempt stopped: time limit

using binary resolution
using first neg lit preferred strategy
not using sos strategy
using dynamic demodulation
using ordered paramodulation
using lex ordering for equality
preferring bigger arities for lex ordering
using clause demodulation
clause length limited to 5
clause depth limited to 12
seconds given: 12

proof attempt stopped: sos exhausted

using binary resolution
using first neg lit preferred strategy
not using sos strategy
using dynamic demodulation
using ordered paramodulation
using lex ordering for equality
preferring bigger arities for lex ordering
using clause demodulation
clause length limited to 5
clause depth limited to 13
seconds given: 12

proof attempt stopped: time limit

using binary resolution
using sos strategy
using dynamic demodulation
using ordered paramodulation
using kb ordering for equality
preferring bigger arities for lex ordering
using clause demodulation
seconds given: 12

proof attempt stopped: sos exhausted

using binary resolution
using first neg lit preferred strategy
not using sos strategy
using dynamic demodulation
using ordered paramodulation
using kb ordering for equality
preferring bigger arities for lex ordering
using clause demodulation
seconds given: 68

proof attempt stopped: time limit

using binary resolution
using first neg lit preferred strategy
not using sos strategy
using dynamic demodulation
using ordered paramodulation
using lex ordering for equality
preferring bigger arities for lex ordering
using clause demodulation
seconds given: 44

********* EMPTY CLAUSE DERIVED *********

********* EMPTY CLAUSE DERIVED *********

timer checkpoints: c(3,40,2,6,0,2,13,50,5,16,0,5,9528,4,711,9663,5,906,9663,1,906,9663,50,908,9663,40,908,9666,0,908,10991,3,1113,12378,4,1211,14866,5,1393,14866,1,1393,14866,50,1394,14866,40,1394,14869,0,1394,17337,3,1656,17892,4,1697,19772,5,1795,19784,1,1795,19784,50,1796,19784,40,1796,19787,0,1796,19794,50,1798,19797,0,1798,28123,3,2840,32590,4,3312,37306,5,3747,37308,1,3747,37308,50,3750,37308,40,3750,37311,0,3750,37318,50,3752,37321,0,3752,44100,3,4227,51250,4,4433,55491,5,4653,55493,1,4653,55493,50,4656,55493,40,4656,55496,0,4656,55497,50,4656,55497,40,4656,55500,0,4656,81692,3,7398,89382,4,8908,98454,5,9857,98462,1,9857,98462,50,9860,98462,40,9860,98465,0,9860,118207,3,12472,118207,4,12472,126466,5,13261,126489,1,13263,126489,50,13266,126489,40,13266,126492,0,13266,136384,3,14336,141920,4,14775,148496,5,15470,148507,1,15470,148507,50,15473,148507,40,15473,148510,0,15473,155256,3,15983,161622,4,16226,162526,5,16474,162526,1,16474,162526,50,16476,162526,40,16476,162529,0,16476,174482,3,17313,178673,4,17695,188717,5,18077,188719,1,18077,188719,50,18079,188719,40,18079,188722,0,18079,194033,3,18627,200190,4,18838,206431,5,19080,206431,1,19080,206431,50,19083,206431,40,19083,206431,40,19083,206434,0,19083,206440,50,19085,206443,0,19085,208105,50,19282,208105,30,19282,208105,40,19282,208108,0,19282,208114,50,19284,208117,0,19284,217556,4,20130,218132,5,20385,218134,1,20386,218134,50,20386,218134,40,20386,218137,0,20386,220622,3,20602,221096,5,20861,221100,1,20861,221100,50,20862,221100,40,20862,221103,0,20862,223588,3,21097,224339,4,21169,225743,5,21263,225752,1,21263,225752,50,21263,225752,40,21263,225755,0,21263,225761,50,21265,225764,0,21497,234777,3,22756,239295,4,23428,242373,5,23998,242376,1,23998,242376,50,23998,242376,40,23998,242379,0,23999,242385,50,24001,242388,0,24001,245322,3,24559,247872,4,24849,250412,5,25102,250422,1,25102,250422,50,25103,250422,40,25103,250425,0,25103,250425,50,25103,250425,40,25103,250428,0,25103,270586,3,28515,277106,4,30352,281446,5,31904,281446,1,31904,281446,50,31904,281446,40,31904,281449,0,31904,302407,3,34111,308900,4,35270,315476,5,36305,315476,1,36305,315476,50,36306,315476,40,36306,315479,0,36306,325270,3,37607,328904,4,38271,331251,5,38908,331259,1,38908,331259,50,38908,331259,40,38908,331262,0,38908,340711,3,39530,341624,4,39820,344416,5,40109,344426,1,40109,344426,50,40110,344426,40,40110,344429,0,40110,354859,3,41131,359394,4,41614,362901,5,42208,362908,1,42209,362908,50,42210,362908,40,42210,362911,0,42210,369955,50,42901,369955,30,42901,369955,40,42901,369958,0,42901,369964,50,42903,369967,0,42903,376063,4,43738,376063,50,43747,376063,40,43747,376066,0,43747,378749,3,43973,380403,4,44095,381450,5,44148,381455,1,44148,381455,50,44148,381455,40,44148,381458,0,44148,382597,3,44449,382597,4,44449,384091,5,44549,384096,1,44549,384096,50,44549,384096,40,44549,384099,0,44549,384105,50,44552,384108,0,44552,397619,3,45818,401730,4,46428,409688,5,47162,409688,1,47162,409688,50,47163,409688,40,47163,409691,0,47164,409697,50,47165,409700,0,47166,415054,3,47936,415770,4,48023,419977,5,48267,419983,1,48267,419983,50,48267,419983,40,48267,419986,0,48267,419986,50,48267,419986,40,48267,419989,0,48267,462267,3,52446,471420,4,53760,484487,5,55068,484541,1,55075,484541,50,55076,484541,40,55076,484544,0,55076,517070,3,57282)

START OF PROOF
484543 [] equal(inverse(multiply(inverse(multiply(X,inverse(multiply(inverse(Y),inverse(multiply(Z,inverse(multiply(inverse(Z),Z)))))))),multiply(X,Z))),Y).
484544 [] -equal(multiply(multiply(a3,b3),c3),multiply(a3,multiply(b3,c3))).
484545 [para:484543.1.1,484543.1.1.1.1.1.2.1.1] equal(inverse(multiply(inverse(multiply(X,inverse(multiply(Y,inverse(multiply(Z,inverse(multiply(inverse(Z),Z)))))))),multiply(X,Z))),multiply(inverse(multiply(U,inverse(multiply(inverse(Y),inverse(multiply(V,inverse(multiply(inverse(V),V)))))))),multiply(U,V))).
484547 [para:484545.1.1,484543.1.1] equal(multiply(inverse(multiply(X,inverse(multiply(inverse(inverse(Y)),inverse(multiply(Z,inverse(multiply(inverse(Z),Z)))))))),multiply(X,Z)),Y).
484548 [para:484545.1.2,484543.1.1.1] equal(inverse(inverse(multiply(inverse(multiply(X,inverse(multiply(Y,inverse(multiply(Z,inverse(multiply(inverse(Z),Z)))))))),multiply(X,Z)))),Y).
484561 [para:484547.1.1,484543.1.1.1.2] equal(inverse(multiply(inverse(multiply(inverse(multiply(X,inverse(multiply(inverse(inverse(Y)),inverse(multiply(Z,inverse(multiply(inverse(Z),Z)))))))),inverse(multiply(inverse(U),inverse(multiply(multiply(X,Z),inverse(multiply(inverse(multiply(X,Z)),multiply(X,Z))))))))),Y)),U).
484568 [para:484547.1.1,484547.1.1.2] equal(multiply(inverse(multiply(inverse(multiply(X,inverse(multiply(inverse(inverse(Y)),inverse(multiply(Z,inverse(multiply(inverse(Z),Z)))))))),inverse(multiply(inverse(inverse(U)),inverse(multiply(multiply(X,Z),inverse(multiply(inverse(multiply(X,Z)),multiply(X,Z))))))))),Y),U).
484751 [para:484561.1.1,484543.1.1.1.1.1.2] equal(inverse(multiply(inverse(multiply(X,Y)),multiply(X,Z))),multiply(inverse(multiply(U,inverse(multiply(inverse(inverse(inverse(multiply(Z,inverse(multiply(inverse(Z),Z)))))),inverse(multiply(V,inverse(multiply(inverse(V),V)))))))),inverse(multiply(inverse(Y),inverse(multiply(multiply(U,V),inverse(multiply(inverse(multiply(U,V)),multiply(U,V))))))))).
484920 [para:484751.1.2,484543.1.1.1.1.1,demod:484547] equal(inverse(multiply(inverse(inverse(multiply(inverse(multiply(X,Y)),multiply(X,Z)))),inverse(multiply(Z,inverse(multiply(inverse(Z),Z)))))),Y).
484944 [para:484751.1.2,484547.1.1.1.1,demod:484547] equal(multiply(inverse(inverse(multiply(inverse(multiply(X,inverse(Y))),multiply(X,Z)))),inverse(multiply(Z,inverse(multiply(inverse(Z),Z))))),Y).
485076 [para:484751.1.2,484751.1.2] equal(inverse(multiply(inverse(multiply(X,Y)),multiply(X,Z))),inverse(multiply(inverse(multiply(U,Y)),multiply(U,Z)))).
485088 [para:485076.1.1,484543.1.1.1.1.1.2.1.1,demod:484543] equal(multiply(inverse(multiply(X,Y)),multiply(X,Z)),multiply(inverse(multiply(U,Y)),multiply(U,Z))).
485089 [para:485076.1.1,484543.1.1.1.1.1.2.1.2.1.2] equal(inverse(multiply(inverse(multiply(X,inverse(multiply(inverse(Y),inverse(multiply(multiply(Z,U),inverse(multiply(inverse(multiply(V,U)),multiply(V,U))))))))),multiply(X,multiply(Z,U)))),Y).
485157 [para:485076.1.1,484568.1.1.1.1.2.1.2.1.2] equal(multiply(inverse(multiply(inverse(multiply(X,inverse(multiply(inverse(inverse(Y)),inverse(multiply(Z,inverse(multiply(inverse(Z),Z)))))))),inverse(multiply(inverse(inverse(U)),inverse(multiply(multiply(X,Z),inverse(multiply(inverse(multiply(V,Z)),multiply(V,Z))))))))),Y),U).
485181 [para:485076.1.1,485076.1.2.1.1] equal(inverse(multiply(inverse(multiply(X,multiply(Y,Z))),multiply(X,U))),inverse(multiply(inverse(multiply(inverse(multiply(V,W)),multiply(V,Z))),multiply(inverse(multiply(Y,W)),U)))).
485365 [para:485076.1.1,485088.1.1.1] equal(multiply(inverse(multiply(inverse(multiply(X,Y)),multiply(X,Z))),multiply(inverse(multiply(U,Y)),V)),multiply(inverse(multiply(W,multiply(U,Z))),multiply(W,V))).
488220 [para:484568.1.1,485089.1.1.1.1.1.2.1.2.1.1,demod:485157] equal(inverse(multiply(inverse(multiply(X,inverse(multiply(inverse(Y),inverse(multiply(Z,inverse(multiply(inverse(multiply(U,V)),multiply(U,V))))))))),multiply(X,Z))),Y).
488358 [para:484547.1.1,488220.1.1.1.1.1.2.1.2.1.2.1.1.1,demod:484547] equal(inverse(multiply(inverse(multiply(X,inverse(multiply(inverse(Y),inverse(multiply(Z,inverse(multiply(inverse(U),U)))))))),multiply(X,Z))),Y).
488582 [para:488358.1.1,484944.1.1.1.1] equal(multiply(inverse(X),inverse(multiply(Y,inverse(multiply(inverse(Y),Y))))),multiply(inverse(X),inverse(multiply(Y,inverse(multiply(inverse(Z),Z)))))).
488865 [para:488582.1.1,484920.1.1.1.1.1.1.1.1,demod:484944] equal(inverse(multiply(X,inverse(multiply(inverse(Y),Y)))),inverse(multiply(X,inverse(multiply(inverse(X),X))))).
488885 [para:488582.1.1,484944.1.1] equal(multiply(inverse(inverse(multiply(inverse(multiply(X,inverse(Y))),multiply(X,Z)))),inverse(multiply(Z,inverse(multiply(inverse(U),U))))),Y).
488886 [para:488582.1.1,484944.1.1.1.1.1.1.1,demod:488885] equal(multiply(X,inverse(multiply(inverse(Y),Y))),multiply(X,inverse(multiply(inverse(X),X)))).
489280 [para:488886.1.1,484920.1.1.1.1.1.1.1.1,demod:488885] equal(inverse(multiply(inverse(X),X)),inverse(multiply(inverse(Y),Y))).
489295 [para:488886.1.1,484944.1.1.1.1.1.1.1,demod:488885] equal(multiply(inverse(X),X),multiply(inverse(Y),Y)).
489514 [para:488886.1.2,488886.1.2] equal(multiply(X,inverse(multiply(inverse(Y),Y))),multiply(X,inverse(multiply(inverse(Z),Z)))).
489628 [para:489295.1.1,484920.1.1.1.1.1.1] equal(inverse(multiply(inverse(inverse(multiply(inverse(X),X))),inverse(multiply(Y,inverse(multiply(inverse(Y),Y)))))),Y).
489641 [para:489295.1.1,484944.1.1.1.1.1] equal(multiply(inverse(inverse(multiply(inverse(X),X))),inverse(multiply(inverse(Y),inverse(multiply(inverse(inverse(Y)),inverse(Y)))))),Y).
489914 [para:489280.1.1,489295.1.1.1] equal(multiply(inverse(multiply(inverse(X),X)),multiply(inverse(Y),Y)),multiply(inverse(Z),Z)).
489916 [para:489280.1.1,489280.1.1.1.1] equal(inverse(multiply(inverse(multiply(inverse(X),X)),multiply(inverse(Y),Y))),inverse(multiply(inverse(Z),Z))).
490115 [para:489514.1.1,489295.1.1] equal(multiply(inverse(inverse(multiply(inverse(X),X))),inverse(multiply(inverse(Y),Y))),multiply(inverse(Z),Z)).
492053 [para:490115.1.1,488582.1.2,demod:489641] equal(inverse(multiply(inverse(X),X)),multiply(inverse(Y),Y)).
492373 [para:492053.1.2,484920.1.1.1.1.1.1] equal(inverse(multiply(inverse(inverse(inverse(multiply(inverse(X),X)))),inverse(multiply(Y,inverse(multiply(inverse(Y),Y)))))),Y).
492697 [para:492053.1.1,488886.1.2.2] equal(multiply(X,inverse(multiply(inverse(Y),Y))),multiply(X,multiply(inverse(Z),Z))).
492711 [para:492053.1.1,489514.1.1.2] equal(multiply(X,multiply(inverse(Y),Y)),multiply(X,inverse(multiply(inverse(Z),Z)))).
492719 [para:492053.1.2,489914.1.1.2] equal(multiply(inverse(multiply(inverse(X),X)),inverse(multiply(inverse(Y),Y))),multiply(inverse(Z),Z)).
492769 [para:492053.1.2,492053.1.1.1] equal(inverse(inverse(multiply(inverse(X),X))),multiply(inverse(Y),Y)).
493404 [para:492769.1.1,484920.1.1.1.1] equal(inverse(multiply(multiply(inverse(X),X),inverse(multiply(Y,inverse(multiply(inverse(Y),Y)))))),Y).
493698 [para:492769.1.1,492053.1.2.1] equal(inverse(multiply(inverse(X),X)),multiply(multiply(inverse(Y),Y),inverse(multiply(inverse(Z),Z)))).
497276 [para:492053.1.1,492697.1.1.2] equal(multiply(X,multiply(inverse(Y),Y)),multiply(X,multiply(inverse(Z),Z))).
520429 [para:492053.1.1,493404.1.1.1.2.1.2] equal(inverse(multiply(multiply(inverse(X),X),inverse(multiply(Y,multiply(inverse(Z),Z))))),Y).
520604 [para:492719.1.2,493404.1.1.1.2.1.2.1] equal(inverse(multiply(multiply(inverse(X),X),inverse(multiply(Y,inverse(multiply(inverse(multiply(inverse(Z),Z)),inverse(multiply(inverse(U),U)))))))),Y).
522048 [para:493698.1.2,484543.1.1.1.2,demod:520604] equal(inverse(multiply(inverse(X),inverse(multiply(inverse(Y),Y)))),X).
522073 [para:493698.1.2,484547.1.1.2,demod:520429,522048] equal(multiply(inverse(inverse(X)),inverse(multiply(inverse(Y),Y))),X).
522108 [para:493698.1.2,484548.1.1.1.1.2,demod:520429,522048,522073] equal(inverse(inverse(multiply(X,inverse(multiply(inverse(Y),Y))))),X).
522917 [para:522048.1.1,484548.1.1.1.1.1,demod:522108] equal(inverse(inverse(multiply(X,multiply(inverse(X),Y)))),Y).
522956 [para:522048.1.1,484561.1.1,demod:492373] equal(multiply(inverse(multiply(X,Y)),inverse(multiply(inverse(Z),inverse(multiply(multiply(X,Y),inverse(multiply(inverse(multiply(X,Y)),multiply(X,Y)))))))),Z).
522985 [para:522048.1.1,484751.1.2.1.1.2.1.1.1.1.1.2,demod:522956,489628,522048] equal(inverse(multiply(inverse(multiply(X,Y)),multiply(X,inverse(multiply(inverse(Z),Z))))),Y).
523024 [para:522048.1.1,484920.1.1.1.2.1.2,demod:522048,522985] equal(inverse(multiply(inverse(X),multiply(inverse(Y),Y))),X).
523324 [para:522048.1.1,493404.1.1.1.2] equal(inverse(multiply(multiply(inverse(X),X),Y)),inverse(Y)).
523465 [para:489280.1.1,522917.1.1.1.1.2.1,demod:523324] equal(inverse(inverse(multiply(inverse(multiply(inverse(X),X)),Y))),Y).
523488 [para:489916.1.2,522917.1.1.1.1.2.1,demod:523324,523024] equal(inverse(inverse(X)),X).
523496 [para:492769.1.1,522917.1.1.1.1.2.1,demod:523465] equal(multiply(multiply(inverse(X),X),Y),Y).
523674 [para:488865.1.1,523488.1.1.1,demod:522108] equal(X,multiply(X,inverse(multiply(inverse(Y),Y)))).
523680 [para:523488.1.1,492697.1.2.2.1,demod:523674] equal(X,multiply(X,multiply(Y,inverse(Y)))).
523681 [para:523488.1.1,497276.1.1.2.1,demod:523680] equal(X,multiply(X,multiply(inverse(Y),Y))).
523682 [para:523488.1.1,492711.1.2.2.1.1,demod:523681] equal(X,multiply(X,inverse(multiply(Y,inverse(Y))))).
523704 [para:523488.1.1,522917.1.1.1.1.2.1,demod:523488] equal(multiply(inverse(X),multiply(X,Y)),Y).
523714 [para:523496.1.1,484547.1.1.1.1,demod:523496,523674,523488] equal(multiply(multiply(X,inverse(Y)),Y),X).
523741 [para:523496.1.1,485088.1.1.1.1,demod:523496] equal(multiply(inverse(X),Y),multiply(inverse(multiply(Z,X)),multiply(Z,Y))).
523759 [para:523680.1.2,484543.1.1.1,demod:523682,523488] equal(multiply(X,inverse(multiply(inverse(Y),X))),Y).
523760 [para:523680.1.2,484545.1.1.1,demod:523714,523741,523759,523682,523488] equal(multiply(X,inverse(multiply(Y,X))),inverse(Y)).
523768 [para:523680.1.2,485076.1.1.1,demod:523741,523488] equal(multiply(X,Y),inverse(multiply(inverse(Y),inverse(X)))).
523774 [para:523680.1.2,485365.1.1.1.1.1.1,demod:523741,523680,523704] equal(multiply(inverse(X),multiply(inverse(Y),Z)),multiply(inverse(multiply(Y,X)),Z)).
523781 [para:523680.1.2,485181.1.1.1,demod:523774,523741,523488] equal(multiply(X,multiply(Y,Z)),inverse(multiply(inverse(Z),multiply(inverse(Y),inverse(X))))).
523916 [para:523760.1.1,485088.1.1.1.1,demod:523741,523488] equal(multiply(X,multiply(Y,Z)),multiply(multiply(X,Y),Z)).
END OF PROOF

Proof found by the following strategy:

using binary resolution
using first neg lit preferred strategy
not using sos strategy
using unit paramodulation strategy
using unit strategy
using dynamic demodulation
using ordered paramodulation
using lex ordering for equality
preferring bigger arities for lex ordering
using clause demodulation
seconds given: 44

Split attempt finished with SUCCESS.

***GANDALF_FOUND_A_REFUTATION***

Global statistics over all passes:

given clauses:    2753
derived clauses:   1426622
kept clauses:      280468
kept size sum:     0
kept mid-nuclei:   2
kept new demods:   29146
forw unit-subs:    742803
forw double-subs: 360
forw overdouble-subs: 0
backward subs:     656
fast unit cutoff:  19
full unit cutoff:  0
dbl  unit cutoff:  0
real runtime    :  583.0
process. runtime:  582.64
specific non-discr-tree subsumption statistics:
tried:           0
length fails:    0
strength fails:  0
predlist fails:  0
aux str. fails:  0
by-lit fails:    0
full subs tried: 0
full subs fail:  0

; program args: ("/home/tptp/Systems/Gandalf---c-2.6B/gandalf" "/tmp/GandalfTemp4115")
```

### Sample Model

```MODEL STARTS
sk2()=0
environment(0)=t
environment(1)=f
an_organisation()=0
appear(0,0)=0
appear(1,0)=1
appear(0,1)=1
appear(1,1)=0
in_environment(0,0)=t
in_environment(1,0)=f
in_environment(0,1)=f
in_environment(1,1)=f
first_movers()=1
equal(0,0)=t
equal(1,0)=f
equal(0,1)=f
equal(1,1)=t
e()=1
number_of_organizations(0,0)=0
number_of_organizations(1,0)=1
number_of_organizations(0,1)=0
number_of_organizations(1,1)=0
zero()=0
greater(0,0)=f
greater(1,0)=t
greater(0,1)=f
greater(1,1)=t
sk1(0,0)=0
sk1(1,0)=0
sk1(0,1)=0
sk1(1,1)=0
subpopulation(0,0,0)=f
subpopulation(1,0,0)=f
subpopulation(0,1,0)=f
subpopulation(1,1,0)=f
subpopulation(0,0,1)=f
subpopulation(1,0,1)=f
subpopulation(0,1,1)=f
subpopulation(1,1,1)=f
cardinality_at_time(0,0)=0
cardinality_at_time(1,0)=0
cardinality_at_time(0,1)=0
cardinality_at_time(1,1)=0
efficient_producers()=0
greater_or_equal(0,0)=t
greater_or_equal(1,0)=t
greater_or_equal(0,1)=f
greater_or_equal(1,1)=t
MODEL ENDS
```

## Otter 3.2

William McCune
Argonne National Laboratory, USA
mccune@mcs.anl.gov
```---------------- PROOF ----------------

1 [] animal(A)| -wolf(A).
2 [] animal(A)| -fox(A).
3 [] animal(A)| -bird(A).
5 [] animal(A)| -snail(A).
6 [] plant(A)| -grain(A).
7 [] eats(A,B)|eats(A,C)| -animal(A)| -plant(B)| -animal(C)| -plant(D)| -much_smaller(C,A)| -eats(C,D).
9 [] much_smaller(A,B)| -snail(A)| -bird(B).
10 [] much_smaller(A,B)| -bird(A)| -fox(B).
11 [] much_smaller(A,B)| -fox(A)| -wolf(B).
13 [] -wolf(A)| -grain(B)| -eats(A,B).
15 [] -bird(A)| -snail(B)| -eats(A,B).
18 [] plant(snail_food_of(A))| -snail(A).
19 [] eats(A,snail_food_of(A))| -snail(A).
20 [] -animal(A)| -animal(B)| -grain(C)| -eats(A,B)| -eats(B,C).
23 [factor,7.4.6] eats(A,B)|eats(A,C)| -animal(A)| -plant(B)| -animal(C)| -much_smaller(C,A)| -eats(C,B).
28 [] wolf(a_wolf).
29 [] fox(a_fox).
30 [] bird(a_bird).
32 [] snail(a_snail).
33 [] grain(a_grain).
34 [hyper,28,1] animal(a_wolf).
35 [hyper,29,11,28] much_smaller(a_fox,a_wolf).
36 [hyper,29,2] animal(a_fox).
37 [hyper,30,10,29] much_smaller(a_bird,a_fox).
38 [hyper,30,3] animal(a_bird).
44 [hyper,32,19] eats(a_snail,snail_food_of(a_snail)).
45 [hyper,32,18] plant(snail_food_of(a_snail)).
46 [hyper,32,9,30] much_smaller(a_snail,a_bird).
47 [hyper,32,5] animal(a_snail).
48 [hyper,33,6] plant(a_grain).
50 [hyper,44,7,38,48,47,45,46] eats(a_bird,a_grain)|eats(a_bird,a_snail).
55 [hyper,50,15,30,32] eats(a_bird,a_grain).
56 [hyper,55,23,36,48,38,37] eats(a_fox,a_grain)|eats(a_fox,a_bird).
62 [hyper,56,20,36,38,33,55] eats(a_fox,a_grain).
63 [hyper,62,23,34,48,36,35] eats(a_wolf,a_grain)|eats(a_wolf,a_fox).
67 [hyper,63,13,28,33] eats(a_wolf,a_fox).
69 [hyper,67,20,34,36,33,62] \$F.

------------ end of proof -------------
```

Koen Claessen, Niklas Sörensson
Chalmers University of Technology and Gothenburg University, Sweden
{koen,nik}@cs.chalmers.se

### Solution Description

When it has found a model, Paradox produces a table of definitions for each constant symbol, function symbol, and predicate symbol. The table is sorted alphabetically. In the table, domain elements are represented as positive natural numbers preceded by a ' (tick).

NOTE: In order to save space in the representation of the model, sometimes, some entries in some of the definition tables are missing. This is not a bug! More detailedly, it might happen that for a model with a domain of size n, for some argument position, only a subset {'1,'2,..,'k} of all domain elements is shown, with k < n. What this means is that the entries for other domain elements 'j (with k < j <= n) occurring at that argument position look the same as entries with 'k at that position. Problem NLP041-1.p is an example where a model is represented in such a way.

### Sample Solution to MGT031-1

```an_organisation = '1

appear('1,'1) = '2
appear('1,'2) = '2
appear('2,'1) = '1
appear('2,'2) = '1

cardinality_at_time('1,'1) = '2
cardinality_at_time('1,'2) = '2
cardinality_at_time('2,'1) = '2
cardinality_at_time('2,'2) = '2

e = '1

efficient_producers = '2

environment('1) : FALSE
environment('2) : TRUE

first_movers = '2

greater('1,'1) : TRUE
greater('1,'2) : TRUE
greater('2,'1) : FALSE
greater('2,'2) : TRUE

greater_or_equal('1,'1) : TRUE
greater_or_equal('1,'2) : TRUE
greater_or_equal('2,'1) : FALSE
greater_or_equal('2,'2) : TRUE

in_environment('1,'1) : TRUE
in_environment('1,'2) : TRUE
in_environment('2,'1) : TRUE
in_environment('2,'2) : TRUE

number_of_organizations('1,'1) = '2
number_of_organizations('1,'2) = '1
number_of_organizations('2,'1) = '2
number_of_organizations('2,'2) = '2

sk1('1,'1) = '2
sk1('1,'2) = '2
sk1('2,'1) = '2
sk1('2,'2) = '2

sk2 = '2

subpopulation('1,'1,'1) : TRUE
subpopulation('1,'1,'2) : TRUE
subpopulation('1,'2,'1) : TRUE
subpopulation('1,'2,'2) : TRUE
subpopulation('2,'1,'1) : TRUE
subpopulation('2,'1,'2) : TRUE
subpopulation('2,'2,'1) : TRUE
subpopulation('2,'2,'2) : TRUE

zero = '1
```

### Sample Solution to NLP041-1.p

```abstraction('1,'1) : FALSE
abstraction('1,'2) : FALSE
abstraction('1,'3) : FALSE
abstraction('1,'4) : TRUE

act('1,'1) : FALSE
act('1,'2) : FALSE
act('1,'3) : TRUE
act('1,'4) : FALSE

actual_world('1) : TRUE

agent('1,'1,'1) : TRUE
agent('1,'1,'2) : TRUE
agent('1,'1,'3) : TRUE
agent('1,'1,'4) : TRUE
agent('1,'2,'1) : TRUE
agent('1,'2,'2) : TRUE
agent('1,'2,'3) : TRUE
agent('1,'2,'4) : TRUE
agent('1,'3,'1) : TRUE
agent('1,'3,'2) : FALSE
agent('1,'3,'3) : FALSE
agent('1,'3,'4) : FALSE
agent('1,'4,'1) : TRUE
agent('1,'4,'2) : TRUE
agent('1,'4,'3) : TRUE
agent('1,'4,'4) : FALSE

animate('1,'1) : TRUE
animate('1,'2) : FALSE
animate('1,'3) : FALSE
animate('1,'4) : FALSE

beverage('1,'1) : FALSE
beverage('1,'2) : TRUE
beverage('1,'3) : FALSE
beverage('1,'4) : FALSE

entity('1,'1) : TRUE
entity('1,'2) : TRUE
entity('1,'3) : FALSE
entity('1,'4) : FALSE

event('1,'1) : FALSE
event('1,'2) : FALSE
event('1,'3) : TRUE
event('1,'4) : FALSE

eventuality('1,'1) : FALSE
eventuality('1,'2) : FALSE
eventuality('1,'3) : TRUE
eventuality('1,'4) : FALSE

existent('1,'1) : TRUE
existent('1,'2) : TRUE
existent('1,'3) : FALSE
existent('1,'4) : FALSE

female('1,'1) : TRUE
female('1,'2) : FALSE
female('1,'3) : FALSE
female('1,'4) : FALSE

food('1,'1) : FALSE
food('1,'2) : TRUE
food('1,'3) : FALSE
food('1,'4) : FALSE

forename('1,'1) : FALSE
forename('1,'2) : FALSE
forename('1,'3) : FALSE
forename('1,'4) : TRUE

general('1,'1) : FALSE
general('1,'2) : FALSE
general('1,'3) : FALSE
general('1,'4) : TRUE

human('1,'1) : TRUE
human('1,'2) : FALSE
human('1,'3) : FALSE
human('1,'4) : FALSE

human_person('1,'1) : TRUE
human_person('1,'2) : FALSE
human_person('1,'3) : FALSE
human_person('1,'4) : FALSE

impartial('1,'1) : TRUE
impartial('1,'2) : TRUE
impartial('1,'3) : FALSE
impartial('1,'4) : FALSE

living('1,'1) : TRUE
living('1,'2) : FALSE
living('1,'3) : FALSE
living('1,'4) : FALSE

mia_forename('1,'1) : FALSE
mia_forename('1,'2) : FALSE
mia_forename('1,'3) : FALSE
mia_forename('1,'4) : TRUE

nonexistent('1,'1) : FALSE
nonexistent('1,'2) : FALSE
nonexistent('1,'3) : TRUE
nonexistent('1,'4) : TRUE

nonhuman('1,'1) : FALSE
nonhuman('1,'2) : TRUE
nonhuman('1,'3) : TRUE
nonhuman('1,'4) : TRUE

nonliving('1,'1) : FALSE
nonliving('1,'2) : TRUE
nonliving('1,'3) : TRUE
nonliving('1,'4) : TRUE

nonreflexive('1,'1) : FALSE
nonreflexive('1,'2) : FALSE
nonreflexive('1,'3) : TRUE
nonreflexive('1,'4) : TRUE

object('1,'1) : FALSE
object('1,'2) : TRUE
object('1,'3) : FALSE
object('1,'4) : FALSE

of('1,'1,'1) : FALSE
of('1,'1,'2) : TRUE
of('1,'1,'3) : TRUE
of('1,'1,'4) : TRUE
of('1,'2,'1) : FALSE
of('1,'2,'2) : TRUE
of('1,'2,'3) : TRUE
of('1,'2,'4) : TRUE
of('1,'3,'1) : FALSE
of('1,'3,'2) : TRUE
of('1,'3,'3) : TRUE
of('1,'3,'4) : TRUE
of('1,'4,'1) : TRUE
of('1,'4,'2) : TRUE
of('1,'4,'3) : TRUE
of('1,'4,'4) : TRUE

order('1,'1) : FALSE
order('1,'2) : FALSE
order('1,'3) : TRUE
order('1,'4) : FALSE

organism('1,'1) : TRUE
organism('1,'2) : FALSE
organism('1,'3) : FALSE
organism('1,'4) : FALSE

past('1,'1) : FALSE
past('1,'2) : FALSE
past('1,'3) : TRUE
past('1,'4) : FALSE

patient('1,'1,'1) : TRUE
patient('1,'1,'2) : TRUE
patient('1,'1,'3) : TRUE
patient('1,'1,'4) : TRUE
patient('1,'2,'1) : TRUE
patient('1,'2,'2) : TRUE
patient('1,'2,'3) : TRUE
patient('1,'2,'4) : TRUE
patient('1,'3,'1) : FALSE
patient('1,'3,'2) : TRUE
patient('1,'3,'3) : TRUE
patient('1,'3,'4) : TRUE
patient('1,'4,'1) : FALSE
patient('1,'4,'2) : FALSE
patient('1,'4,'3) : FALSE
patient('1,'4,'4) : TRUE

relation('1,'1) : FALSE
relation('1,'2) : FALSE
relation('1,'3) : FALSE
relation('1,'4) : TRUE

relname('1,'1) : FALSE
relname('1,'2) : FALSE
relname('1,'3) : FALSE
relname('1,'4) : TRUE

shake_beverage('1,'1) : FALSE
shake_beverage('1,'2) : TRUE
shake_beverage('1,'3) : FALSE
shake_beverage('1,'4) : FALSE

singleton('1,'1) : TRUE
singleton('1,'2) : TRUE
singleton('1,'3) : TRUE
singleton('1,'4) : TRUE

skc5 = '1

skc6 = '3

skc7 = '2

skc8 = '4

skc9 = '1

specific('1,'1) : TRUE
specific('1,'2) : TRUE
specific('1,'3) : TRUE
specific('1,'4) : FALSE

substance_matter('1,'1) : FALSE
substance_matter('1,'2) : TRUE
substance_matter('1,'3) : FALSE
substance_matter('1,'4) : FALSE

thing('1,'1) : TRUE
thing('1,'2) : TRUE
thing('1,'3) : TRUE
thing('1,'4) : TRUE

unisex('1,'1) : FALSE
unisex('1,'2) : TRUE
unisex('1,'3) : TRUE
unisex('1,'4) : TRUE

woman('1,'1) : TRUE
woman('1,'2) : FALSE
woman('1,'3) : FALSE
woman('1,'4) : FALSE
```

## THEO J2003

Monty Newborn
newborn@cs.mcgill.ca

TBA.

### Sample solution for SYN075-1

```Axioms:
1: ~E.x:y ~big_fxz big_fyz
2: ~E.x:y ~big_fzx big_fzy
3: ~E.x:y ~E.y:z E.x:z
4 >~E.x:a ~E.y:b big_fxy
5: ~E.x:y E.hxz:hyz
6 >~E.x:y E.hzx:hzy
7: ~E.x:y E.fx:fy
8: ~E.x:y E.gx:gy
9 >~big_fxy E.x:a
10: ~big_fxy E.y:b
11: ~E.x:y E.y:x
12 >E.x:x

Negated conclusion:
13S ~big_fxfy E.x:gy big_fhyzfy ~big_fhyzfy
14S ~E.x:gy big_fxfy big_fhyzfy E.hyz:z
15S ~E.x:gy big_fxfy ~E.hyz:z ~big_fhyzfy
16S>~E.fx:x ~E.hxy:y ~big_fhxyfx
17S>~E.fx:x big_fhxyfx E.hxy:y
18S>~big_fxfy ~E.x:gy E.fy:y
19S>~E.x:gy big_fxfy E.fy:y

---------------

Phase 0 clauses used in proof:
20S>(19b*18a) ~E.x:gy E.fy:y

Phases 1 and 2 clauses used in proof:
21S>(20a,12a) E.fx:x

22S>(20b,17a) ~E.x:gy big_fhyzfy E.hyz:z
23S>(22b,9a)  ~E.x:gy E.hyz:z E.hyz:a
24S>(23a,12a) E.hxy:y E.hxy:a
25S>(24ab)    E.hxa:a

26S>(21a,4a)  ~E.x:b big_ffax
27S>[26b,21a] ~E.x:b big_fax
28S>[27a,12a] big_fab

29S>(16b,6b)  ~E.fx:x ~big_fhxhxyfx ~E.hxy:y
30S>[29a,21a] ~E.x:x ~big_fhxhxyfx ~E.hxy:y
31S>[30b,21a] ~E.x:x ~big_fhxhxyx ~E.hxy:y
32S>[31a,12a] ~big_fhxhxyx ~E.hxy:y
33S>(32b,6b)  ~big_fhxhxhxyx ~E.hxy:y
34: 33|{a/y} ~big_fhxhxhxax ~E.hxa:a
35S>(34b,25a) ~big_fhxhxhxax
36S>[35a,25a] ~big_fhxhxax
37S>[36a,25a] ~big_fhxax
38S>[37a,25a] ~big_fax
39S>(38a,28a) []
```

## Vampire 5.0

Alexandre Riazanov, Andrei Voronkov
University of Manchester, England
{riazanoa,voronkov}@cs.man.ac.uk

### How to Read Vampire Proofs

A proof is a collection of clauses. The clauses are printed as follows:
```<clause> : <number>"." <clause body> <auxilliary info> "["<background list>"]"
% nonempty clause

: <number>'. #'  <auxilliary info> '['<background list>']'
% empty clause

<clause body> : <literals>
% all literals are selected
: <literals>1 | <literals>2
% <literals>1 are selected
% <literals>2 are nonselected

<background list> : <flags><ancestors>

<ancestors> :        % empty (must be an input clause)
: <number> ("," <number>)*

<flags> : (<flag> )+

<flag> : "in"      % input clause
: "pp"      % clause obtained by preprocessing
: "br"      % generated by binary resolution
: "hr"      % generated by hyperresolution
: "fs"      % generated by forward superposition
: "bs"      % generated by backward superposition
: "er"      % generated by equality resolution
: "ef"      % generated by equality factoring
: "fd"      % simplified by forward demodulation
: "bd"      % simplified by backward demodulation
: "ers"     % simplified by equality resolution
: "fsr"     % simplified by forward subsumption resolution
: "sp"      % splitting was used
: "rea"     % "reanimated" passive clause (selected in Discount algorithm)
: "nm"      % the clause is a part of a name introduction in
% splitting, or obtained by preprocessing from such
% a clause
: "ns"      % negative selection was used (does not mean that
% all the selected literals are negative)

<literals> :  <literal> [" \/ " <literals>]

<literal> : <standard literal>
: <equational literal>
: <splitting literal>

<standard literal> : ["~"]<atom> % "~" is for negation
<atom> : <predicate symbol> % propositional variable
: <predicate symbol><arguments>
<equational literal> : <term> = <term>  % unoriented positive equality
: <term> != <term> % unoriented negative equality
: <term> == <term>  % oriented positive equality
: <term> !== <term> % oriented negative equality

<splitting literal> : "["<predicate symbol>"]"

<term> : <variable>
: <constant>
: <function symbol><arguments>
<variable> : "X"<number>
<arguments> : "("<term> (","<term>)* ")"
```

### Tabulated Proofs

When Vampire is called with the options --proof and --tab <tabulation file>, it writes the proof in Prolog syntax into the tabulation file. Every proof step is a Prolog fact of the form
```vproof(<JobId>,[<clause body> <clause number> <ancestors> <flags>]).
```
<JobId> is an atom, uniquely identifying the job that produced the proof. <ancestors> is a list of ancestor numbers. <flags> is a list of flags, every flag is an atom. <clause body> is a list of literals.
```<literal> : "++"<atom>      % unselected positive literal
: "+++"<atom>     % selected positive literal
: "--"<atom>      % unselected negative literal
: "---"<atom>     % selected negative literal

<atom> : <term>
: "("<term>" = "<term>")"   % unoriented equality
: "("<term>" => "<term>")"  % oriented equality

<term> : <function symbol>["("<term>(","<term>)*")"]
: <variable>
```
<function symbol> is a Prolog alphanumeric identifier. <variable> is a quoted Prolog atom "'X""'" To process such proofs with Prolog, '++','+++','--' and '---' should be declared prefix operators and '=>' infix operator of appropriate precedence.

Problem SET497-6.p
```%======================== Proof: =========================
% 1. member(z,z) /3/3/0/ 0pe [in ]
% 2. member(z,diagonalise(element_relation)) /4/4/0/ 0pe [in ]
% 120. X0=null_class \/ intersection(X0,regular(X0))=null_class /9/9/0/ 2pe [in ]
% 121. X0=null_class \/ member(regular(X0),X0) /7/7/0/ 1pe [in ]
% 144. union(X0,singleton(X0))=successor(X0) /7/7/0/ 1pe [in ]
% 161. complement(intersection(complement(X0),complement(X1)))=union(X0,X1) /10/10/0/ 1pe [in ]
% 162. member(X0,complement(X1)) \/ ~member(X0,universal_class) \/ member(X0,X1) /10/10/0/ 0pe [in ]
% 163. ~member(X0,complement(X1)) \/ ~member(X0,X1) /7/7/0/ 0pe [in ]
% 164. ~member(X0,X2) \/ ~member(X0,X1) \/ member(X0,intersection(X1,X2)) /11/11/0/ 0pe [in ]
% 165. ~member(X0,intersection(X1,X2)) \/ member(X0,X2) /8/8/0/ 0pe [in ]
% 166. ~member(X0,intersection(X1,X2)) \/ member(X0,X1) /8/8/0/ 0pe [in ]
% 175. unordered_pair(X0,X0)=singleton(X0) /6/6/0/ 1pe [in ]
% 178. ~member(X0,universal_class) \/ member(X0,unordered_pair(X0,X1)) /8/8/0/ 0pe [in ]
% 179. X0=X1 \/ ~member(X0,unordered_pair(X1,X2)) \/ X0=X2 /11/11/0/ 2pe [in ]
% 183. subclass(X0,universal_class) /3/3/0/ 0pe [in ]
% 186. ~member(X2,X0) \/ ~subclass(X0,X1) \/ member(X2,X1) /9/9/0/ 0pe [in ]
% 190. member(z,z) /3/3/0/ 0pe [pp 1]
% 191. member(z,diagonalise(element_relation)) /4/4/0/ 0pe [pp 2]
% 237. intersection(X0,regular(X0))==null_class | X0=null_class /9/9/5/ 2pe [pp 120]
% 238. member(regular(X0),X0) | X0=null_class /7/7/3/ 1pe [pp 121]
% 261. union(X0,singleton(X0))==successor(X0) /7/7/3/ 1pe [pp 144]
% 278. complement(intersection(complement(X0),complement(X1)))==union(X0,X1) /10/10/4/ 1pe [pp 161]% 279. ~member(X0,universal_class) | member(X0,complement(X1)) \/ member(X0,X1) /10/10/7/ 0pe [pp 162]
% 280. ~member(X0,complement(X1)) | ~member(X0,X1) /7/7/3/ 0pe [pp 163]
% 281. ~member(X0,X1) | ~member(X0,X2) \/ member(X0,intersection(X1,X2)) /11/11/8/ 0pe [pp ns 164]
% 282. ~member(X0,intersection(X1,X2)) | member(X0,X2) /8/8/3/ 0pe [pp 165]
% 283. ~member(X0,intersection(X1,X2)) | member(X0,X1) /8/8/3/ 0pe [pp 166]
% 292. unordered_pair(X0,X0)==singleton(X0) /6/6/3/ 1pe [pp 175]
% 295. ~member(X0,universal_class) | member(X0,unordered_pair(X0,X1)) /8/8/5/ 0pe [pp 178]
% 296. ~member(X0,unordered_pair(X1,X2)) | X0=X1 \/ X0=X2 /11/11/6/ 2pe [pp 179]
% 299. subclass(X0,universal_class) /3/3/0/ 0pe [pp 183]
% 302. ~subclass(X0,X1) | ~member(X2,X0) \/ member(X2,X1) /9/9/6/ 0pe [pp 186]
% 303. member(z,z) /3/3/0/ 0pe [pp 190]
% 304. member(z,diagonalise(element_relation)) /4/4/0/ 0pe [pp 191]
% 350. intersection(X0,regular(X0))==null_class | X0=null_class /9/9/5/ 2pe [pp 237]
% 351. member(regular(X0),X0) | X0=null_class /7/7/3/ 1pe [pp 238]
% 374. union(X0,singleton(X0))==successor(X0) /7/7/3/ 1pe [pp 261]
% 391. complement(intersection(complement(X0),complement(X1)))==union(X0,X1) /10/10/4/ 1pe [pp 278]% 392. ~member(X0,universal_class) | member(X0,complement(X1)) \/ member(X0,X1) /10/10/7/ 0pe [pp 279]
% 393. ~member(X0,complement(X1)) | ~member(X0,X1) /7/7/3/ 0pe [pp 280]
% 394. ~member(X0,X1) | ~member(X0,X2) \/ member(X0,intersection(X2,X1)) /11/11/8/ 0pe [pp ns 281]
% 395. ~member(X0,intersection(X1,X2)) | member(X0,X2) /8/8/3/ 0pe [pp 282]
% 396. ~member(X0,intersection(X1,X2)) | member(X0,X1) /8/8/3/ 0pe [pp 283]
% 405. unordered_pair(X0,X0)==singleton(X0) /6/6/3/ 1pe [pp 292]
% 408. ~member(X0,universal_class) | member(X0,unordered_pair(X0,X1)) /8/8/5/ 0pe [pp 295]
% 409. ~member(X0,unordered_pair(X1,X2)) | X0=X1 \/ X0=X2 /11/11/6/ 2pe [pp 296]
% 412. subclass(X0,universal_class) /3/3/0/ 0pe [pp 299]
% 415. ~subclass(X0,X1) | ~member(X2,X0) \/ member(X2,X1) /9/9/6/ 0pe [pp 302]
% 424. member(z,z) /3/3/0/ 0pe [pp 303]
% 425. member(z,diagonalise(element_relation)) /4/4/0/ 0pe [pp 304]
% 457. intersection(X0,regular(X0))==null_class | X0=null_class /9/9/5/ 2pe [pp 350]
% 458. member(regular(X0),X0) | X0=null_class /7/7/3/ 1pe [pp 351]
% 474. union(X0,singleton(X0))==successor(X0) /7/7/3/ 1pe [pp 374]
% 491. complement(intersection(complement(X0),complement(X1)))==union(X0,X1) /10/10/4/ 1pe [pp 391]% 492. ~member(X0,universal_class) | member(X0,complement(X1)) \/ member(X0,X1) /10/10/7/ 0pe [pp 392]
% 493. ~member(X0,complement(X1)) | ~member(X0,X1) /7/7/3/ 0pe [pp 393]
% 494. ~member(X0,X1) | ~member(X0,X2) \/ member(X0,intersection(X1,X2)) /11/11/8/ 0pe [pp ns 394]
% 495. ~member(X0,intersection(X1,X2)) | member(X0,X2) /8/8/3/ 0pe [pp 395]
% 496. ~member(X0,intersection(X1,X2)) | member(X0,X1) /8/8/3/ 0pe [pp 396]
% 505. unordered_pair(X0,X0)==singleton(X0) /6/6/3/ 1pe [pp 405]
% 508. ~member(X0,universal_class) | member(X0,unordered_pair(X0,X1)) /8/8/5/ 0pe [pp 408]
% 509. ~member(X0,unordered_pair(X1,X2)) | X0=X1 \/ X0=X2 /11/11/6/ 2pe [pp 409]
% 512. subclass(X0,universal_class) /3/3/0/ 0pe [pp 412]
% 515. ~subclass(X0,X1) | ~member(X2,X0) \/ member(X2,X1) /9/9/6/ 0pe [pp 415]
% 526. member(z,z) /3/3/0/ 0pe [pp 424]
% 527. member(z,diagonalise(element_relation)) /4/4/0/ 0pe [pp 425]
% 556. intersection(X0,regular(X0))==null_class | X0=null_class /9/9/5/ 2pe [pp 457]
% 557. member(regular(X0),X0) | X0=null_class /7/7/3/ 1pe [pp 458]
% 573. union(X0,singleton(X0))==successor(X0) /7/7/3/ 1pe [pp 474]
% 590. complement(intersection(complement(X0),complement(X1)))==union(X0,X1) /10/10/4/ 1pe [pp 491]% 591. ~member(X0,universal_class) | member(X0,complement(X1)) \/ member(X0,X1) /10/10/7/ 0pe [pp 492]
% 592. ~member(X0,complement(X1)) | ~member(X0,X1) /7/7/3/ 0pe [pp 493]
% 593. ~member(X0,X1) | ~member(X0,X2) \/ member(X0,intersection(X2,X1)) /11/11/8/ 0pe [pp ns 494]
% 594. ~member(X0,intersection(X1,X2)) | member(X0,X2) /8/8/3/ 0pe [pp 495]
% 595. ~member(X0,intersection(X1,X2)) | member(X0,X1) /8/8/3/ 0pe [pp 496]
% 604. unordered_pair(X0,X0)==singleton(X0) /6/6/3/ 1pe [pp 505]
% 607. ~member(X0,universal_class) | member(X0,unordered_pair(X0,X1)) /8/8/5/ 0pe [pp 508]
% 608. ~member(X0,unordered_pair(X1,X2)) | X0=X1 \/ X0=X2 /11/11/6/ 2pe [pp 509]
% 611. subclass(X0,universal_class) /3/3/0/ 0pe [pp 512]
% 614. ~subclass(X0,X1) | ~member(X2,X0) \/ member(X2,X1) /9/9/6/ 0pe [pp 515]
% * 620. member(z,z) /3/3/0/ 0pe vip [pp 526]
% * 621. member(z,diagonalise(element_relation)) /4/4/0/ 0pe vip [pp 527]
% * 650. intersection(X0,regular(X0))==null_class | X0=null_class /9/9/5/ 2pe vip [pp 556]
% * 651. member(regular(X0),X0) | X0=null_class /7/7/3/ 1pe vip [pp 557]
% * 667. union(X0,singleton(X0))==successor(X0) /7/7/3/ 1pe [pp 573]
% * 685. complement(intersection(complement(X0),complement(X1)))==union(X0,X1) /10/10/4/ 1pe [pp 590]
% * 687. ~member(X0,universal_class) | member(X0,complement(X1)) \/ member(X0,X1) /10/10/7/ 0pe [pp 591]
% * 688. ~member(X0,complement(X1)) | ~member(X0,X1) /7/7/3/ 0pe vip [pp 592]
% * 689. ~member(X0,X1) | ~member(X0,X2) \/ member(X0,intersection(X1,X2)) /11/11/8/ 0pe [pp ns 593]
% * 690. ~member(X0,intersection(X1,X2)) | member(X0,X2) /8/8/3/ 0pe vip [pp 594]
% * 691. ~member(X0,intersection(X1,X2)) | member(X0,X1) /8/8/3/ 0pe vip [pp 595]
% * 700. unordered_pair(X0,X0)==singleton(X0) /6/6/3/ 1pe [pp 604]
% * 703. ~member(X0,universal_class) | member(X0,unordered_pair(X0,X1)) /8/8/5/ 0pe [pp 607]
% * 704. ~member(X0,unordered_pair(X1,X2)) | X0=X1 \/ X0=X2 /11/11/6/ 2pe [pp 608]
% * 707. subclass(X0,universal_class) /3/3/0/ 0pe vip [pp 611]
% * 710. ~subclass(X0,X1) | ~member(X2,X0) \/ member(X2,X1) /9/9/6/ 0pe [pp 614]
% * 753. ~member(regular(complement(X0)),X0) | complement(X0)==null_class /9/9/4/ 1pe [br 651,688]
% * 757. ~member(z,X0) | member(z,intersection(z,X0)) /8/8/5/ 0pe [br 620,689]
% * 758. ~member(z,X0) | member(z,intersection(diagonalise(element_relation),X0)) /9/9/6/ 0pe [br 621,689]
% * 761. member(regular(intersection(X0,X1)),X1) | intersection(X0,X1)==null_class /11/11/5/ 1pe [br 651,690]
% * 768. member(regular(intersection(X0,X1)),X0) | intersection(X0,X1)==null_class /11/11/5/ 1pe [br 651,691]
% * 798. ~member(X0,singleton(X1)) | X0=X1 /7/7/3/ 1pe vip [fs 700,704]
% * 822. ~member(X0,X1) | member(X0,universal_class) /6/6/3/ 0pe [br 707,710]
% * 999. member(z,universal_class) /3/3/0/ 0pe vip [br 620,822]
% * 1000. member(regular(X0),universal_class) | X0=null_class /7/7/3/ 1pe vip [br 651,822]
% * 1005. member(z,unordered_pair(z,X0)) /5/5/0/ 0pe vip [br 703,999]
% * 1007. member(z,complement(X0)) | member(z,X0) /7/7/3/ 0pe vip [br 687,999]
% * 1083. member(z,singleton(z)) /4/4/0/ 0pe vip [fs 700,1005]
% * 1085. ~member(z,X0) | member(z,intersection(singleton(z),X0)) /9/9/6/ 0pe [br 689,1083]
% * 1568. regular(singleton(X0))==X0 | singleton(X0)==null_class /9/9/6/ 2pe vip [br 651,798]
% * 1669. member(z,intersection(complement(X0),complement(X1))) | member(z,union(X0,X1)) /12/12/5/ 0pe [fs 685,1007]
% * 2598. complement(universal_class)==null_class /4/4/2/ 1pe vip [br 1000,753]
% * 2619. ~member(X0,null_class) /3/3/0/ 0pe vip [bs fsr 822,688,2598]
% * 2730. member(z,intersection(diagonalise(element_relation),singleton(z))) /7/7/0/ 0pe vip [br 1083,758]
% * 2771. ~member(z,X0) | member(z,intersection(intersection(diagonalise(element_relation),singleton(z)),X0)) /12/12/9/ 0pe [br 689,2730]
% * 2824. intersection(X0,null_class)==null_class /5/5/2/ 1pe vip [br 2619,761]
% * 2971. intersection(null_class,X0)==null_class /5/5/2/ 1pe vip [br 2619,768]
% * 20420. member(z,intersection(singleton(z),z)) /6/6/0/ 0pe vip [br 620,1085]
% * 23048. intersection(singleton(X0),X0)==null_class | singleton(X0)==null_class /10/10/6/ 2pe [bs 650,1568]
% * 110195. member(z,union(X0,X1)) | member(z,complement(X0)) /9/9/4/ 0pe [br 691,1669]
% * 110426. member(z,complement(X0)) | member(z,successor(X0)) /8/8/4/ 0pe [fs 667,110195]
% * 110427. ~member(z,X0) | member(z,successor(X0)) /7/7/4/ 0pe [br 688,110426]
% * 110491. member(z,successor(z)) /4/4/0/ 0pe vip [br 620,110427]
% * 110884. ~member(z,X0) | member(z,intersection(successor(z),X0)) /9/9/6/ 0pe [br 689,110491]
% * 120575. member(z,intersection(successor(z),intersection(singleton(z),z))) /9/9/0/ 0pe [br 20420,110884]
% * 144335. member(z,intersection(intersection(diagonalise(element_relation),singleton(z)),universal_class)) /9/9/0/ 0pe vip [br 999,2771]
% 144354. member(z,intersection(z,intersection(intersection(diagonalise(element_relation),singleton(z)),universal_class))) /11/11/0/ 0pe [br 757,144335]
% 144460. singleton(z)==null_class /4/4/2/ 1pe vip [bs fd fsr 2619,2824,120575,23048]
% 144462. # /1/0/0/ 0pe vip [fd bd fsr 2619,2824,2971,2824,144354,144460]
%==================  End of proof. ========================
```

Problem SET497-6.p
```vproof('9520011456592226',[[+++member(z,z)],1,[],[in]]).
vproof('9520011456592226',[[+++member(z,diagonalise(element_relation))],2,[],[in]]).
vproof('9520011456592226',[[+++('X0' = null_class),+++(intersection('X0',regular('X0')) = null_class)],120,[],[in]]).
vproof('9520011456592226',[[+++('X0' = null_class),+++member(regular('X0'),'X0')],121,[],[in]]).
vproof('9520011456592226',[[+++(union('X0',singleton('X0')) = successor('X0'))],144,[],[in]]).
vproof('9520011456592226',[[+++(complement(intersection(complement('X0'),complement('X1'))) = union('X0','X1'))],161,[],[in]]).
vproof('9520011456592226',[[+++member('X0',complement('X1')),---member('X0',universal_class),+++member('X0','X1')],162,[],[in]]).
vproof('9520011456592226',[[---member('X0',complement('X1')),---member('X0','X1')],163,[],[in]]).
vproof('9520011456592226',[[---member('X0','X2'),---member('X0','X1'),+++member('X0',intersection('X1','X2'))],164,[],[in]]).
vproof('9520011456592226',[[---member('X0',intersection('X1','X2')),+++member('X0','X2')],165,[],[in]]).
vproof('9520011456592226',[[---member('X0',intersection('X1','X2')),+++member('X0','X1')],166,[],[in]]).
vproof('9520011456592226',[[+++(unordered_pair('X0','X0') = singleton('X0'))],175,[],[in]]).
vproof('9520011456592226',[[---member('X0',universal_class),+++member('X0',unordered_pair('X0','X1'))],178,[],[in]]).
vproof('9520011456592226',[[+++('X0' = 'X1'),---member('X0',unordered_pair('X1','X2')),+++('X0' = 'X2')],179,[],[in]]).
vproof('9520011456592226',[[+++subclass('X0',universal_class)],183,[],[in]]).
vproof('9520011456592226',[[---member('X2','X0'),---subclass('X0','X1'),+++member('X2','X1')],186,[],[in]]).
vproof('9520011456592226',[[+++member(z,z)],190,[1],[pp]]).
vproof('9520011456592226',[[+++member(z,diagonalise(element_relation))],191,[2],[pp]]).
vproof('9520011456592226',[[+++(intersection('X0',regular('X0')) => null_class),++('X0' = null_class)],237,[120],[pp]]).
vproof('9520011456592226',[[+++member(regular('X0'),'X0'),++('X0' = null_class)],238,[121],[pp]]).
vproof('9520011456592226',[[+++(union('X0',singleton('X0')) => successor('X0'))],261,[144],[pp]]).
vproof('9520011456592226',[[+++(complement(intersection(complement('X0'),complement('X1'))) => union('X0','X1'))],278,[161],[pp]]).
vproof('9520011456592226',[[---member('X0',universal_class),++member('X0',complement('X1')),++member('X0','X1')],279,[162],[pp]]).
vproof('9520011456592226',[[---member('X0',complement('X1')),--member('X0','X1')],280,[163],[pp]]).
vproof('9520011456592226',[[---member('X0','X1'),--member('X0','X2'),++member('X0',intersection('X1','X2'))],281,[164],[pp]]).
vproof('9520011456592226',[[---member('X0',intersection('X1','X2')),++member('X0','X2')],282,[165],[pp]]).
vproof('9520011456592226',[[---member('X0',intersection('X1','X2')),++member('X0','X1')],283,[166],[pp]]).
vproof('9520011456592226',[[+++(unordered_pair('X0','X0') => singleton('X0'))],292,[175],[pp]]).
vproof('9520011456592226',[[---member('X0',universal_class),++member('X0',unordered_pair('X0','X1'))],295,[178],[pp]]).
vproof('9520011456592226',[[---member('X0',unordered_pair('X1','X2')),++('X0' = 'X1'),++('X0' = 'X2')],296,[179],[pp]]).
vproof('9520011456592226',[[+++subclass('X0',universal_class)],299,[183],[pp]]).
vproof('9520011456592226',[[---subclass('X0','X1'),--member('X2','X0'),++member('X2','X1')],302,[186],[pp]]).
vproof('9520011456592226',[[+++member(z,z)],303,[190],[pp]]).
vproof('9520011456592226',[[+++member(z,diagonalise(element_relation))],304,[191],[pp]]).
vproof('9520011456592226',[[+++(intersection('X0',regular('X0')) => null_class),++('X0' = null_class)],350,[237],[pp]]).
vproof('9520011456592226',[[+++member(regular('X0'),'X0'),++('X0' = null_class)],351,[238],[pp]]).
vproof('9520011456592226',[[+++(union('X0',singleton('X0')) => successor('X0'))],374,[261],[pp]]).
vproof('9520011456592226',[[+++(complement(intersection(complement('X0'),complement('X1'))) => union('X0','X1'))],391,[278],[pp]]).
vproof('9520011456592226',[[---member('X0',universal_class),++member('X0',complement('X1')),++member('X0','X1')],392,[279],[pp]]).
vproof('9520011456592226',[[---member('X0',complement('X1')),--member('X0','X1')],393,[280],[pp]]).
vproof('9520011456592226',[[---member('X0','X1'),--member('X0','X2'),++member('X0',intersection('X2','X1'))],394,[281],[pp]]).
vproof('9520011456592226',[[---member('X0',intersection('X1','X2')),++member('X0','X2')],395,[282],[pp]]).
vproof('9520011456592226',[[---member('X0',intersection('X1','X2')),++member('X0','X1')],396,[283],[pp]]).
vproof('9520011456592226',[[+++(unordered_pair('X0','X0') => singleton('X0'))],405,[292],[pp]]).
vproof('9520011456592226',[[---member('X0',universal_class),++member('X0',unordered_pair('X0','X1'))],408,[295],[pp]]).
vproof('9520011456592226',[[---member('X0',unordered_pair('X1','X2')),++('X0' = 'X1'),++('X0' = 'X2')],409,[296],[pp]]).
vproof('9520011456592226',[[+++subclass('X0',universal_class)],412,[299],[pp]]).
vproof('9520011456592226',[[---subclass('X0','X1'),--member('X2','X0'),++member('X2','X1')],415,[302],[pp]]).
vproof('9520011456592226',[[+++member(z,z)],424,[303],[pp]]).
vproof('9520011456592226',[[+++member(z,diagonalise(element_relation))],425,[304],[pp]]).
vproof('9520011456592226',[[+++(intersection('X0',regular('X0')) => null_class),++('X0' = null_class)],457,[350],[pp]]).
vproof('9520011456592226',[[+++member(regular('X0'),'X0'),++('X0' = null_class)],458,[351],[pp]]).
vproof('9520011456592226',[[+++(union('X0',singleton('X0')) => successor('X0'))],474,[374],[pp]]).
vproof('9520011456592226',[[+++(complement(intersection(complement('X0'),complement('X1'))) => union('X0','X1'))],491,[391],[pp]]).
vproof('9520011456592226',[[---member('X0',universal_class),++member('X0',complement('X1')),++member('X0','X1')],492,[392],[pp]]).
vproof('9520011456592226',[[---member('X0',complement('X1')),--member('X0','X1')],493,[393],[pp]]).
vproof('9520011456592226',[[---member('X0','X1'),--member('X0','X2'),++member('X0',intersection('X1','X2'))],494,[394],[pp]]).
vproof('9520011456592226',[[---member('X0',intersection('X1','X2')),++member('X0','X2')],495,[395],[pp]]).
vproof('9520011456592226',[[---member('X0',intersection('X1','X2')),++member('X0','X1')],496,[396],[pp]]).
vproof('9520011456592226',[[+++(unordered_pair('X0','X0') => singleton('X0'))],505,[405],[pp]]).
vproof('9520011456592226',[[---member('X0',universal_class),++member('X0',unordered_pair('X0','X1'))],508,[408],[pp]]).
vproof('9520011456592226',[[---member('X0',unordered_pair('X1','X2')),++('X0' = 'X1'),++('X0' = 'X2')],509,[409],[pp]]).
vproof('9520011456592226',[[+++subclass('X0',universal_class)],512,[412],[pp]]).
vproof('9520011456592226',[[---subclass('X0','X1'),--member('X2','X0'),++member('X2','X1')],515,[415],[pp]]).
vproof('9520011456592226',[[+++member(z,z)],526,[424],[pp]]).
vproof('9520011456592226',[[+++member(z,diagonalise(element_relation))],527,[425],[pp]]).
vproof('9520011456592226',[[+++(intersection('X0',regular('X0')) => null_class),++('X0' = null_class)],556,[457],[pp]]).
vproof('9520011456592226',[[+++member(regular('X0'),'X0'),++('X0' = null_class)],557,[458],[pp]]).
vproof('9520011456592226',[[+++(union('X0',singleton('X0')) => successor('X0'))],573,[474],[pp]]).
vproof('9520011456592226',[[+++(complement(intersection(complement('X0'),complement('X1'))) => union('X0','X1'))],590,[491],[pp]]).
vproof('9520011456592226',[[---member('X0',universal_class),++member('X0',complement('X1')),++member('X0','X1')],591,[492],[pp]]).
vproof('9520011456592226',[[---member('X0',complement('X1')),--member('X0','X1')],592,[493],[pp]]).
vproof('9520011456592226',[[---member('X0','X1'),--member('X0','X2'),++member('X0',intersection('X2','X1'))],593,[494],[pp]]).
vproof('9520011456592226',[[---member('X0',intersection('X1','X2')),++member('X0','X2')],594,[495],[pp]]).
vproof('9520011456592226',[[---member('X0',intersection('X1','X2')),++member('X0','X1')],595,[496],[pp]]).
vproof('9520011456592226',[[+++(unordered_pair('X0','X0') => singleton('X0'))],604,[505],[pp]]).
vproof('9520011456592226',[[---member('X0',universal_class),++member('X0',unordered_pair('X0','X1'))],607,[508],[pp]]).
vproof('9520011456592226',[[---member('X0',unordered_pair('X1','X2')),++('X0' = 'X1'),++('X0' = 'X2')],608,[509],[pp]]).
vproof('9520011456592226',[[+++subclass('X0',universal_class)],611,[512],[pp]]).
vproof('9520011456592226',[[---subclass('X0','X1'),--member('X2','X0'),++member('X2','X1')],614,[515],[pp]]).
vproof('9520011456592226',[[+++member(z,z)],620,[526],[pp]]).
vproof('9520011456592226',[[+++member(z,diagonalise(element_relation))],621,[527],[pp]]).
vproof('9520011456592226',[[+++(intersection('X0',regular('X0')) => null_class),++('X0' = null_class)],650,[556],[pp]]).
vproof('9520011456592226',[[+++member(regular('X0'),'X0'),++('X0' = null_class)],651,[557],[pp]]).
vproof('9520011456592226',[[+++(union('X0',singleton('X0')) => successor('X0'))],667,[573],[pp]]).
vproof('9520011456592226',[[+++(complement(intersection(complement('X0'),complement('X1'))) => union('X0','X1'))],685,[590],[pp]]).
vproof('9520011456592226',[[---member('X0',universal_class),++member('X0',complement('X1')),++member('X0','X1')],687,[591],[pp]]).
vproof('9520011456592226',[[---member('X0',complement('X1')),--member('X0','X1')],688,[592],[pp]]).
vproof('9520011456592226',[[---member('X0','X1'),--member('X0','X2'),++member('X0',intersection('X1','X2'))],689,[593],[pp]]).
vproof('9520011456592226',[[---member('X0',intersection('X1','X2')),++member('X0','X2')],690,[594],[pp]]).
vproof('9520011456592226',[[---member('X0',intersection('X1','X2')),++member('X0','X1')],691,[595],[pp]]).
vproof('9520011456592226',[[+++(unordered_pair('X0','X0') => singleton('X0'))],700,[604],[pp]]).
vproof('9520011456592226',[[---member('X0',universal_class),++member('X0',unordered_pair('X0','X1'))],703,[607],[pp]]).
vproof('9520011456592226',[[---member('X0',unordered_pair('X1','X2')),++('X0' = 'X1'),++('X0' = 'X2')],704,[608],[pp]]).
vproof('9520011456592226',[[+++subclass('X0',universal_class)],707,[611],[pp]]).
vproof('9520011456592226',[[---subclass('X0','X1'),--member('X2','X0'),++member('X2','X1')],710,[614],[pp]]).
vproof('9520011456592226',[[---member(regular(complement('X0')),'X0'),++(complement('X0') => null_class)],753,[651,688],[br]]).
vproof('9520011456592226',[[---member(z,'X0'),++member(z,intersection(z,'X0'))],757,[620,689],[br]]).
vproof('9520011456592226',[[---member(z,'X0'),++member(z,intersection(diagonalise(element_relation),'X0'))],758,[621,689],[br]]).
vproof('9520011456592226',[[+++member(regular(intersection('X0','X1')),'X1'),++(intersection('X0','X1') => null_class)],761,[651,690],[br]]).
vproof('9520011456592226',[[+++member(regular(intersection('X0','X1')),'X0'),++(intersection('X0','X1') => null_class)],768,[651,691],[br]]).
vproof('9520011456592226',[[---member('X0',singleton('X1')),++('X0' = 'X1')],798,[700,704],[fs]]).
vproof('9520011456592226',[[---member('X0','X1'),++member('X0',universal_class)],822,[707,710],[br]]).
vproof('9520011456592226',[[+++member(z,universal_class)],999,[620,822],[br]]).
vproof('9520011456592226',[[+++member(regular('X0'),universal_class),++('X0' = null_class)],1000,[651,822],[br]]).
vproof('9520011456592226',[[+++member(z,unordered_pair(z,'X0'))],1005,[703,999],[br]]).
vproof('9520011456592226',[[+++member(z,complement('X0')),++member(z,'X0')],1007,[687,999],[br]]).
vproof('9520011456592226',[[+++member(z,singleton(z))],1083,[700,1005],[fs]]).
vproof('9520011456592226',[[---member(z,'X0'),++member(z,intersection(singleton(z),'X0'))],1085,[689,1083],[br]]).
vproof('9520011456592226',[[+++(regular(singleton('X0')) => 'X0'),++(singleton('X0') => null_class)],1568,[651,798],[br]]).
vproof('9520011456592226',[[+++member(z,intersection(complement('X0'),complement('X1'))),++member(z,union('X0','X1'))],1669,[685,1007],[fs]]).
vproof('9520011456592226',[[+++(complement(universal_class) => null_class)],2598,[1000,753],[br]]).
vproof('9520011456592226',[[---member('X0',null_class)],2619,[822,688,2598],[bs,fsr]]).
vproof('9520011456592226',[[+++member(z,intersection(diagonalise(element_relation),singleton(z)))],2730,[1083,758],[br]]).
vproof('9520011456592226',[[---member(z,'X0'),++member(z,intersection(intersection(diagonalise(element_relation),singleton(z)),'X0'))],2771,[689,2730],[br]]).
vproof('9520011456592226',[[+++(intersection('X0',null_class) => null_class)],2824,[2619,761],[br]]).
vproof('9520011456592226',[[+++(intersection(null_class,'X0') => null_class)],2971,[2619,768],[br]]).
vproof('9520011456592226',[[+++member(z,intersection(singleton(z),z))],20420,[620,1085],[br]]).
vproof('9520011456592226',[[+++(intersection(singleton('X0'),'X0') => null_class),++(singleton('X0') => null_class)],23048,[650,1568],[bs]]).
vproof('9520011456592226',[[+++member(z,union('X0','X1')),++member(z,complement('X0'))],107744,[691,1669],[br]]).
vproof('9520011456592226',[[+++member(z,complement('X0')),++member(z,successor('X0'))],108260,[667,107744],[fs]]).
vproof('9520011456592226',[[---member(z,'X0'),++member(z,successor('X0'))],108261,[688,108260],[br]]).
vproof('9520011456592226',[[+++member(z,successor(z))],108325,[620,108261],[br]]).
vproof('9520011456592226',[[---member(z,'X0'),++member(z,intersection(successor(z),'X0'))],108718,[689,108325],[br]]).
vproof('9520011456592226',[[+++member(z,intersection(successor(z),intersection(singleton(z),z)))],118516,[20420,108718],[br]]).
vproof('9520011456592226',[[+++member(z,intersection(intersection(diagonalise(element_relation),singleton(z)),universal_class))],142519,[999,2771],[br]]).
vproof('9520011456592226',[[+++member(z,intersection(z,intersection(intersection(diagonalise(element_relation),singleton(z)),universal_class)))],142538,[757,142519],[br]]).
vproof('9520011456592226',[[+++(singleton(z) => null_class)],142584,[2619,2824,118516,23048],[bs,fd,fsr]]).
vproof('9520011456592226',[[],142585,[2619,2824,2971,2824,142538,142584],[fd,bd,fsr]]).
```

## Vampire 6.0

Alexandre Riazanov, Andrei Voronkov
University of Manchester, England
{riazanoa,voronkov}@cs.man.ac.uk

### KEY FOR VAMPIRE PROOFS

1. "Refutation found" means that the input set of clauses/formulas is unsatisfiable. "Proof by contradiction found" means that the input set contains a FOF conjecture, which has been negated and the resulting set has been refuted. Negation of the conjecture is implicit (will change later).
2. The syntax of clauses and formulas is self-explanatory. # denotes the empty clause.
3. All input clauses/formulas contributed to a refutation are given in the following form:
```*********** [<number>] ***************
<clause/formula body>```
4. All proof steps are of the following form:
```******* [<premise number>,..,<premise number>-><conclusion number>] **********
<premise>
.
.
.
<premise>
-------------------------------
<conclusion> ```
Premises and conclusions can be formulas or clauses.
5. A proof step is either a clausification step or a combined application of some inference rules of the kernel (resolution, paramodulation or splitting). Not all proof steps are deductive, i.e. the conclusion may not be logically implied by the premises. Some steps are only satisfiability-preserving, e.g., clausification steps involving Skolemisation and steps that use splitting or negative equality splitting.
Example 1. A step from the sample solution for SYN551+1
```*********** [11->20] ***********
(~X0=f(g(X0)) \/
((sk1=f(g(sk1)) &
~sk1=sk0) &
sk0=f(g(sk0))) \/
~X3=g(f(X3)) \/
((sk3=g(f(sk3)) &
~sk3=sk2) &
sk2=g(f(sk2)))) &
((sk4=f(g(sk4)) &
((~X8=f(g(X8)) \/
X8=X7) \/
~X7=f(g(X7)))) \/
(sk5=g(f(sk5)) &
((~X11=g(f(X11)) \/
X11=X10) \/
~X10=g(f(X10)))))
-----------------------------
sk2=g(f(sk2)) \/ ~X3=g(f(X3)) \/ sk0=f(g(sk0)) \/ ~X0=f(g(X0))```
The conclusion [20] is one of the clauses obtained by clausification of the premise [11]. The constant sk5 was introduced by skolemisation.

Example 2. Three steps from the sample solution for SYN551+1

```*********** [20->25] ***********
sk2=g(f(sk2)) \/ ~X3=g(f(X3)) \/ sk0=f(g(sk0)) \/ ~X0=f(g(X0))
-----------------------------
~g(f(X0))=X0 \/ p__2

*********** [20->31] ***********
sk2=g(f(sk2)) \/ ~X3=g(f(X3)) \/ sk0=f(g(sk0)) \/ ~X0=f(g(X0))
-----------------------------
~f(g(X0))=X0 \/ p__3

*********** [20->42] ***********
sk2=g(f(sk2)) \/ ~X3=g(f(X3)) \/ sk0=f(g(sk0)) \/ ~X0=f(g(X0))
-----------------------------
f(g(sk0))=sk0 \/ g(f(sk2))=sk2 \/ ~p__2 \/ ~p__3 ```
These steps together form a splitting inference. In the first two we introduce names p__2 and p__3 for the components ~X3=g(f(X3)) and ~X0=f(g(X0)) of the clause [20]. The last one is obtained by folding the components.

Example 3. Two steps from the sample solution for COL003-20:

```*********** [9->10] ***********
~apply(strong_fixed_point,fixed_pt)=apply(fixed_pt,apply(strong_fixed_point,fixe
d_pt))
-----------------------------
~p__0(apply(strong_fixed_point,fixed_pt)

*********** [9->12] ***********
~apply(strong_fixed_point,fixed_pt)=apply(fixed_pt,apply(strong_fixed_point,fixe
d_pt))
-----------------------------
p__0(apply(fixed_pt,apply(strong_fixed_point,fixed_pt))) ```
These steps form a negative equality splitting. Again, p__0 is a new predicate.

### Sample solution for SYN075-1

```Refutation found. Thanks to Tanya!
*********** [12] ***********
~X0=a \/ ~X1=b \/ big_f(X0,X1)
*********** [12->20] ***********
~X0=a \/ ~X1=b \/ big_f(X0,X1)
-----------------------------
big_f(a,b)
*********** [20->21] ***********
big_f(a,b)
-----------------------------
big_f(a,b)
*********** [10] ***********
~big_f(X0,X1) \/ X0=a
*********** [10->22] ***********
~big_f(X0,X1) \/ X0=a
-----------------------------
~big_f(X0,X1) \/ X0=a
*********** [22->23] ***********
~big_f(X0,X1) \/ X0=a
-----------------------------
~big_f(X0,X1) \/ X0=a
*********** [13] ***********
~big_f(X1,f(X0)) \/ ~X1=g(X0) \/ f(X0)=X0
*********** [13->24] ***********
~big_f(X1,f(X0)) \/ ~X1=g(X0) \/ f(X0)=X0
-----------------------------
~big_f(g(X0),f(X0)) \/ f(X0)=X0
*********** [15] ***********
~X1=g(X0) \/ big_f(X1,f(X0)) \/ f(X0)=X0
*********** [24,15->25] ***********
~big_f(g(X0),f(X0)) \/ f(X0)=X0
~X1=g(X0) \/ big_f(X1,f(X0)) \/ f(X0)=X0
-----------------------------
f(X0)=X0
*********** [25->26] ***********
f(X0)=X0
-----------------------------
f(X0)=X0
*********** [18] ***********
~f(X0)=X0 \/ big_f(h(X0,X2),f(X0)) \/ h(X0,X2)=X2
*********** [18->27] ***********
~f(X0)=X0 \/ big_f(h(X0,X2),f(X0)) \/ h(X0,X2)=X2
-----------------------------
~f(X0)=X0 \/ h(X0,X1)=X1 \/ big_f(h(X0,X1),f(X0))
*********** [26,26,27->28] ***********
f(X0)=X0
f(X0)=X0
~f(X0)=X0 \/ h(X0,X1)=X1 \/ big_f(h(X0,X1),f(X0))
-----------------------------
big_f(h(X0,X1),X0) \/ h(X0,X1)=X1
*********** [23,28->29] ***********
~big_f(X0,X1) \/ X0=a
big_f(h(X0,X1),X0) \/ h(X0,X1)=X1
-----------------------------
h(X0,X1)=a \/ h(X0,X1)=X1
*********** [29->30] ***********
h(X0,X1)=a \/ h(X0,X1)=X1
-----------------------------
h(X0,a)=a
*********** [19] ***********
~f(X0)=X0 \/ ~h(X0,X2)=X2 \/ ~big_f(h(X0,X2),f(X0))
*********** [19->31] ***********
~f(X0)=X0 \/ ~h(X0,X2)=X2 \/ ~big_f(h(X0,X2),f(X0))
-----------------------------
~big_f(h(X0,X1),f(X0)) \/ ~h(X0,X1)=X1 \/ ~f(X0)=X0
*********** [26,26,31->32] ***********
f(X0)=X0
f(X0)=X0
~big_f(h(X0,X1),f(X0)) \/ ~h(X0,X1)=X1 \/ ~f(X0)=X0
-----------------------------
~h(X0,X1)=X1 \/ ~big_f(h(X0,X1),X0)
*********** [30,32,30->33] ***********
h(X0,a)=a
~h(X0,X1)=X1 \/ ~big_f(h(X0,X1),X0)
h(X0,a)=a
-----------------------------
~big_f(a,X0)
*********** [21,33->34] ***********
big_f(a,b)
~big_f(a,X0)
-----------------------------
#
======= End of refutation ======= ```

### Sample solution for SYN551+1

```Proof by contradiction found. Thanks to Tanya!
=========== Refutation ==========
*********** [6] ***********
~((? X0)X0=f(g(X0)) &
(! X1 X2)
(X1=f(g(X1)) & X2=f(g(X2)) =>
X1=X2) <=>
(? X3)X3=g(f(X3)) &
(! X4 X5)
(X4=g(f(X4)) & X5=g(f(X5)) =>
X4=X5))
*********** [6->7] ***********
~((? X0)X0=f(g(X0)) &
(! X1 X2)
(X1=f(g(X1)) & X2=f(g(X2)) =>
X1=X2) <=>
(? X3)X3=g(f(X3)) &
(! X4 X5)
(X4=g(f(X4)) & X5=g(f(X5)) =>
X4=X5))
-----------------------------
(? X0)X0=f(g(X0)) &
(! X1 X2)
(~X1=f(g(X1)) \/
~X2=f(g(X2)) \/
X1=X2) <~>
(? X3)X3=g(f(X3)) &
(! X4 X5)
(~X4=g(f(X4)) \/
~X5=g(f(X5)) \/
X4=X5)
*********** [7->8] ***********
(? X0)X0=f(g(X0)) &
(! X1 X2)
(~X1=f(g(X1)) \/
~X2=f(g(X2)) \/
X1=X2) <~>
(? X3)X3=g(f(X3)) &
(! X4 X5)
(~X4=g(f(X4)) \/
~X5=g(f(X5)) \/
X4=X5)
-----------------------------
((? X0)X0=f(g(X0)) &
(! X1 X2)
(~X1=f(g(X1)) \/
~X2=f(g(X2)) \/
X1=X2) =>
~((? X3)X3=g(f(X3)) &
(! X4 X5)
(~X4=g(f(X4)) \/
~X5=g(f(X5)) \/
X4=X5))) &
(~((? X0)X0=f(g(X0)) &
(! X1 X2)
(~X1=f(g(X1)) \/
~X2=f(g(X2)) \/
X1=X2)) =>
(? X3)X3=g(f(X3)) &
(! X4 X5)
(~X4=g(f(X4)) \/
~X5=g(f(X5)) \/
X4=X5))
*********** [8->9] ***********
((? X0)X0=f(g(X0)) &
(! X1 X2)
(~X1=f(g(X1)) \/
~X2=f(g(X2)) \/
X1=X2) =>
~((? X3)X3=g(f(X3)) &
(! X4 X5)
(~X4=g(f(X4)) \/
~X5=g(f(X5)) \/
X4=X5))) &
(~((? X0)X0=f(g(X0)) &
(! X1 X2)
(~X1=f(g(X1)) \/
~X2=f(g(X2)) \/
X1=X2)) =>
(? X3)X3=g(f(X3)) &
(! X4 X5)
(~X4=g(f(X4)) \/
~X5=g(f(X5)) \/
X4=X5))
-----------------------------
((! X0)
~X0=f(g(X0)) \/
(? X1 X2)
(X1=f(g(X1)) &
X2=f(g(X2)) &
~X1=X2) \/
(! X3)
~X3=g(f(X3)) \/
(? X4 X5)
(X4=g(f(X4)) &
X5=g(f(X5)) &
~X4=X5)) &
(((? X0)X0=f(g(X0)) &
(! X1 X2)
(~X1=f(g(X1)) \/
~X2=f(g(X2)) \/
X1=X2)) \/
((? X3)X3=g(f(X3)) &
(! X4 X5)
(~X4=g(f(X4)) \/
~X5=g(f(X5)) \/
X4=X5)))
*********** [9->10] ***********
((! X0)
~X0=f(g(X0)) \/
(? X1 X2)
(X1=f(g(X1)) &
X2=f(g(X2)) &
~X1=X2) \/
(! X3)
~X3=g(f(X3)) \/
(? X4 X5)
(X4=g(f(X4)) &
X5=g(f(X5)) &
~X4=X5)) &
(((? X0)X0=f(g(X0)) &
(! X1 X2)
(~X1=f(g(X1)) \/
~X2=f(g(X2)) \/
X1=X2)) \/
((? X3)X3=g(f(X3)) &
(! X4 X5)
(~X4=g(f(X4)) \/
~X5=g(f(X5)) \/
X4=X5)))
-----------------------------
((! X0)
~X0=f(g(X0)) \/
(? X1)
((? X2)
(X2=f(g(X2)) &
~X2=X1) &
X1=f(g(X1))) \/
(! X3)
~X3=g(f(X3)) \/
(? X4)
((? X5)
(X5=g(f(X5)) &
~X5=X4) &
X4=g(f(X4)))) &
(((? X6)X6=f(g(X6)) &
(! X7)
((! X8)
(~X8=f(g(X8)) \/
X8=X7) \/
~X7=f(g(X7)))) \/
((? X9)X9=g(f(X9)) &
(! X10)
((! X11)
(~X11=g(f(X11)) \/
X11=X10) \/
~X10=g(f(X10)))))
*********** [10->11] ***********
((! X0)
~X0=f(g(X0)) \/
(? X1)
((? X2)
(X2=f(g(X2)) &
~X2=X1) &
X1=f(g(X1))) \/
(! X3)
~X3=g(f(X3)) \/
(? X4)
((? X5)
(X5=g(f(X5)) &
~X5=X4) &
X4=g(f(X4)))) &
(((? X6)X6=f(g(X6)) &
(! X7)
((! X8)
(~X8=f(g(X8)) \/
X8=X7) \/
~X7=f(g(X7)))) \/
((? X9)X9=g(f(X9)) &
(! X10)
((! X11)
(~X11=g(f(X11)) \/
X11=X10) \/
~X10=g(f(X10)))))
-----------------------------
(~X0=f(g(X0)) \/
((sk1=f(g(sk1)) &
~sk1=sk0) &
sk0=f(g(sk0))) \/
~X3=g(f(X3)) \/
((sk3=g(f(sk3)) &
~sk3=sk2) &
sk2=g(f(sk2)))) &
((sk4=f(g(sk4)) &
((~X8=f(g(X8)) \/
X8=X7) \/
~X7=f(g(X7)))) \/
(sk5=g(f(sk5)) &
((~X11=g(f(X11)) \/
X11=X10) \/
~X10=g(f(X10)))))
*********** [11->20] ***********
(~X0=f(g(X0)) \/
((sk1=f(g(sk1)) &
~sk1=sk0) &
sk0=f(g(sk0))) \/
~X3=g(f(X3)) \/
((sk3=g(f(sk3)) &
~sk3=sk2) &
sk2=g(f(sk2)))) &
((sk4=f(g(sk4)) &
((~X8=f(g(X8)) \/
X8=X7) \/
~X7=f(g(X7)))) \/
(sk5=g(f(sk5)) &
((~X11=g(f(X11)) \/
X11=X10) \/
~X10=g(f(X10)))))
-----------------------------
sk2=g(f(sk2)) \/ ~X3=g(f(X3)) \/ sk0=f(g(sk0)) \/ ~X0=f(g(X0))
*********** [20->25] ***********
sk2=g(f(sk2)) \/ ~X3=g(f(X3)) \/ sk0=f(g(sk0)) \/ ~X0=f(g(X0))
-----------------------------
~g(f(X0))=X0 \/ p__2
*********** [25->26] ***********
~g(f(X0))=X0 \/ p__2
-----------------------------
~g(f(X0))=X0 \/ p__2
*********** [11->21] ***********
(~X0=f(g(X0)) \/
((sk1=f(g(sk1)) &
~sk1=sk0) &
sk0=f(g(sk0))) \/
~X3=g(f(X3)) \/
((sk3=g(f(sk3)) &
~sk3=sk2) &
sk2=g(f(sk2)))) &
((sk4=f(g(sk4)) &
((~X8=f(g(X8)) \/
X8=X7) \/
~X7=f(g(X7)))) \/
(sk5=g(f(sk5)) &
((~X11=g(f(X11)) \/
X11=X10) \/
~X10=g(f(X10)))))
-----------------------------
sk5=g(f(sk5)) \/ sk4=f(g(sk4))
*********** [21->27] ***********
sk5=g(f(sk5)) \/ sk4=f(g(sk4))
-----------------------------
f(g(sk4))=sk4 \/ g(f(sk5))=sk5
*********** [27->28] ***********
f(g(sk4))=sk4 \/ g(f(sk5))=sk5
-----------------------------
f(g(sk4))=sk4 \/ g(f(sk5))=sk5
*********** [28,26->29] ***********
f(g(sk4))=sk4 \/ g(f(sk5))=sk5
~g(f(X0))=X0 \/ p__2
-----------------------------
g(f(sk5))=sk5 \/ p__2
*********** [26,29->30] ***********
~g(f(X0))=X0 \/ p__2
g(f(sk5))=sk5 \/ p__2
-----------------------------
p__2
*********** [20->31] ***********
sk2=g(f(sk2)) \/ ~X3=g(f(X3)) \/ sk0=f(g(sk0)) \/ ~X0=f(g(X0))
-----------------------------
~f(g(X0))=X0 \/ p__3
*********** [31->32] ***********
~f(g(X0))=X0 \/ p__3
-----------------------------
~f(g(X0))=X0 \/ p__3
*********** [28,32->33] ***********
f(g(sk4))=sk4 \/ g(f(sk5))=sk5
~f(g(X0))=X0 \/ p__3
-----------------------------
g(f(sk5))=sk5 \/ p__3
*********** [32,33->34] ***********
~f(g(X0))=X0 \/ p__3
g(f(sk5))=sk5 \/ p__3
-----------------------------
p__3
*********** [11->16] ***********
(~X0=f(g(X0)) \/
((sk1=f(g(sk1)) &
~sk1=sk0) &
sk0=f(g(sk0))) \/
~X3=g(f(X3)) \/
((sk3=g(f(sk3)) &
~sk3=sk2) &
sk2=g(f(sk2)))) &
((sk4=f(g(sk4)) &
((~X8=f(g(X8)) \/
X8=X7) \/
~X7=f(g(X7)))) \/
(sk5=g(f(sk5)) &
((~X11=g(f(X11)) \/
X11=X10) \/
~X10=g(f(X10)))))
-----------------------------
~sk3=sk2 \/ ~X3=g(f(X3)) \/ ~sk1=sk0 \/ ~X0=f(g(X0))
*********** [16->35] ***********
~sk3=sk2 \/ ~X3=g(f(X3)) \/ ~sk1=sk0 \/ ~X0=f(g(X0))
-----------------------------
~sk0=sk1 \/ ~sk2=sk3 \/ ~p__2 \/ ~p__3
*********** [35->36] ***********
~sk0=sk1 \/ ~sk2=sk3 \/ ~p__2 \/ ~p__3
-----------------------------
~sk0=sk1 \/ ~sk2=sk3 \/ ~p__2 \/ ~p__3
*********** [11->22] ***********
(~X0=f(g(X0)) \/
((sk1=f(g(sk1)) &
~sk1=sk0) &
sk0=f(g(sk0))) \/
~X3=g(f(X3)) \/
((sk3=g(f(sk3)) &
~sk3=sk2) &
sk2=g(f(sk2)))) &
((sk4=f(g(sk4)) &
((~X8=f(g(X8)) \/
X8=X7) \/
~X7=f(g(X7)))) \/
(sk5=g(f(sk5)) &
((~X11=g(f(X11)) \/
X11=X10) \/
~X10=g(f(X10)))))
-----------------------------
~X10=g(f(X10)) \/ X11=X10 \/ ~X11=g(f(X11)) \/ sk4=f(g(sk4))
*********** [22->37] ***********
~X10=g(f(X10)) \/ X11=X10 \/ ~X11=g(f(X11)) \/ sk4=f(g(sk4))
-----------------------------
f(g(sk4))=sk4 \/ ~p__0
*********** [37->38] ***********
f(g(sk4))=sk4 \/ ~p__0
-----------------------------
f(g(sk4))=sk4 \/ ~p__0
*********** [38,26->39] ***********
f(g(sk4))=sk4 \/ ~p__0
~g(f(X0))=X0 \/ p__2
-----------------------------
p__2 \/ ~p__0
*********** [11->24] ***********
(~X0=f(g(X0)) \/
((sk1=f(g(sk1)) &
~sk1=sk0) &
sk0=f(g(sk0))) \/
~X3=g(f(X3)) \/
((sk3=g(f(sk3)) &
~sk3=sk2) &
sk2=g(f(sk2)))) &
((sk4=f(g(sk4)) &
((~X8=f(g(X8)) \/
X8=X7) \/
~X7=f(g(X7)))) \/
(sk5=g(f(sk5)) &
((~X11=g(f(X11)) \/
X11=X10) \/
~X10=g(f(X10)))))
-----------------------------
~X10=g(f(X10)) \/ X11=X10 \/ ~X11=g(f(X11)) \/ ~X7=f(g(X7)) \/ X8=X7 \/ ~X8=f(g(X8))
*********** [24->40] ***********
~X10=g(f(X10)) \/ X11=X10 \/ ~X11=g(f(X11)) \/ ~X7=f(g(X7)) \/ X8=X7 \/ ~X8=f(g(X8))
-----------------------------
~f(g(X0))=X0 \/ ~f(g(X1))=X1 \/ X0=X1 \/ ~p__0
*********** [40->41] ***********
~f(g(X0))=X0 \/ ~f(g(X1))=X1 \/ X0=X1 \/ ~p__0
-----------------------------
~f(g(X0))=X0 \/ ~f(g(X1))=X1 \/ X0=X1 \/ ~p__0
*********** [20->42] ***********
sk2=g(f(sk2)) \/ ~X3=g(f(X3)) \/ sk0=f(g(sk0)) \/ ~X0=f(g(X0))
-----------------------------
f(g(sk0))=sk0 \/ g(f(sk2))=sk2 \/ ~p__2 \/ ~p__3
*********** [42->43] ***********
f(g(sk0))=sk0 \/ g(f(sk2))=sk2 \/ ~p__2 \/ ~p__3
-----------------------------
f(g(sk0))=sk0 \/ g(f(sk2))=sk2 \/ ~p__2 \/ ~p__3
*********** [39,32,41,43->44] ***********
p__2 \/ ~p__0
~f(g(X0))=X0 \/ p__3
~f(g(X0))=X0 \/ ~f(g(X1))=X1 \/ X0=X1 \/ ~p__0
f(g(sk0))=sk0 \/ g(f(sk2))=sk2 \/ ~p__2 \/ ~p__3
-----------------------------
g(f(sk2))=sk2 \/ ~p__0 \/ ~p__5
*********** [41,38->45] ***********
~f(g(X0))=X0 \/ ~f(g(X1))=X1 \/ X0=X1 \/ ~p__0
f(g(sk4))=sk4 \/ ~p__0
-----------------------------
~f(g(X0))=X0 \/ sk4=X0 \/ ~p__0
*********** [44,45->46] ***********
g(f(sk2))=sk2 \/ ~p__0 \/ ~p__5
~f(g(X0))=X0 \/ sk4=X0 \/ ~p__0
-----------------------------
f(sk2)=sk4 \/ ~p__0 \/ ~p__5
*********** [44,46->47] ***********
g(f(sk2))=sk2 \/ ~p__0 \/ ~p__5
f(sk2)=sk4 \/ ~p__0 \/ ~p__5
-----------------------------
g(sk4)=sk2 \/ ~p__0 \/ ~p__5
*********** [11->18] ***********
(~X0=f(g(X0)) \/
((sk1=f(g(sk1)) &
~sk1=sk0) &
sk0=f(g(sk0))) \/
~X3=g(f(X3)) \/
((sk3=g(f(sk3)) &
~sk3=sk2) &
sk2=g(f(sk2)))) &
((sk4=f(g(sk4)) &
((~X8=f(g(X8)) \/
X8=X7) \/
~X7=f(g(X7)))) \/
(sk5=g(f(sk5)) &
((~X11=g(f(X11)) \/
X11=X10) \/
~X10=g(f(X10)))))
-----------------------------
sk3=g(f(sk3)) \/ ~X3=g(f(X3)) \/ sk0=f(g(sk0)) \/ ~X0=f(g(X0))
*********** [18->48] ***********
sk3=g(f(sk3)) \/ ~X3=g(f(X3)) \/ sk0=f(g(sk0)) \/ ~X0=f(g(X0))
-----------------------------
f(g(sk0))=sk0 \/ g(f(sk3))=sk3 \/ ~p__2 \/ ~p__3
*********** [48->49] ***********
f(g(sk0))=sk0 \/ g(f(sk3))=sk3 \/ ~p__2 \/ ~p__3
-----------------------------
f(g(sk0))=sk0 \/ g(f(sk3))=sk3 \/ ~p__2 \/ ~p__3
*********** [39,32,41,49->50] ***********
p__2 \/ ~p__0
~f(g(X0))=X0 \/ p__3
~f(g(X0))=X0 \/ ~f(g(X1))=X1 \/ X0=X1 \/ ~p__0
f(g(sk0))=sk0 \/ g(f(sk3))=sk3 \/ ~p__2 \/ ~p__3
-----------------------------
g(f(sk3))=sk3 \/ ~p__0 \/ ~p__5
*********** [50,45->51] ***********
g(f(sk3))=sk3 \/ ~p__0 \/ ~p__5
~f(g(X0))=X0 \/ sk4=X0 \/ ~p__0
-----------------------------
f(sk3)=sk4 \/ ~p__0 \/ ~p__5
*********** [47,50,51->52] ***********
g(sk4)=sk2 \/ ~p__0 \/ ~p__5
g(f(sk3))=sk3 \/ ~p__0 \/ ~p__5
f(sk3)=sk4 \/ ~p__0 \/ ~p__5
-----------------------------
sk2=sk3 \/ ~p__0 \/ ~p__5
*********** [11->19] ***********
(~X0=f(g(X0)) \/
((sk1=f(g(sk1)) &
~sk1=sk0) &
sk0=f(g(sk0))) \/
~X3=g(f(X3)) \/
((sk3=g(f(sk3)) &
~sk3=sk2) &
sk2=g(f(sk2)))) &
((sk4=f(g(sk4)) &
((~X8=f(g(X8)) \/
X8=X7) \/
~X7=f(g(X7)))) \/
(sk5=g(f(sk5)) &
((~X11=g(f(X11)) \/
X11=X10) \/
~X10=g(f(X10)))))
-----------------------------
~sk3=sk2 \/ ~X3=g(f(X3)) \/ sk0=f(g(sk0)) \/ ~X0=f(g(X0))
*********** [19->53] ***********
~sk3=sk2 \/ ~X3=g(f(X3)) \/ sk0=f(g(sk0)) \/ ~X0=f(g(X0))
-----------------------------
~sk2=sk3 \/ f(g(sk0))=sk0 \/ ~p__2 \/ ~p__3
*********** [53->54] ***********
~sk2=sk3 \/ f(g(sk0))=sk0 \/ ~p__2 \/ ~p__3
-----------------------------
~sk2=sk3 \/ f(g(sk0))=sk0 \/ ~p__2 \/ ~p__3
*********** [30,34,54,52->55] ***********
p__2
p__3
~sk2=sk3 \/ f(g(sk0))=sk0 \/ ~p__2 \/ ~p__3
sk2=sk3 \/ ~p__0 \/ ~p__5
-----------------------------
f(g(sk0))=sk0 \/ ~p__0 \/ ~p__5
*********** [45,55->56] ***********
~f(g(X0))=X0 \/ sk4=X0 \/ ~p__0
f(g(sk0))=sk0 \/ ~p__0 \/ ~p__5
-----------------------------
sk0=sk4 \/ ~p__0 \/ ~p__5
*********** [52,30,34,36,56->57] ***********
sk2=sk3 \/ ~p__0 \/ ~p__5
p__2
p__3
~sk0=sk1 \/ ~sk2=sk3 \/ ~p__2 \/ ~p__3
sk0=sk4 \/ ~p__0 \/ ~p__5
-----------------------------
~sk1=sk4 \/ ~p__0 \/ ~p__5
*********** [11->13] ***********
(~X0=f(g(X0)) \/
((sk1=f(g(sk1)) &
~sk1=sk0) &
sk0=f(g(sk0))) \/
~X3=g(f(X3)) \/
((sk3=g(f(sk3)) &
~sk3=sk2) &
sk2=g(f(sk2)))) &
((sk4=f(g(sk4)) &
((~X8=f(g(X8)) \/
X8=X7) \/
~X7=f(g(X7)))) \/
(sk5=g(f(sk5)) &
((~X11=g(f(X11)) \/
X11=X10) \/
~X10=g(f(X10)))))
-----------------------------
~sk3=sk2 \/ ~X3=g(f(X3)) \/ sk1=f(g(sk1)) \/ ~X0=f(g(X0))
*********** [13->58] ***********
~sk3=sk2 \/ ~X3=g(f(X3)) \/ sk1=f(g(sk1)) \/ ~X0=f(g(X0))
-----------------------------
~sk2=sk3 \/ f(g(sk1))=sk1 \/ ~p__2 \/ ~p__3
*********** [58->59] ***********
~sk2=sk3 \/ f(g(sk1))=sk1 \/ ~p__2 \/ ~p__3
-----------------------------
~sk2=sk3 \/ f(g(sk1))=sk1 \/ ~p__2 \/ ~p__3
*********** [30,34,59,52->60] ***********
p__2
p__3
~sk2=sk3 \/ f(g(sk1))=sk1 \/ ~p__2 \/ ~p__3
sk2=sk3 \/ ~p__0 \/ ~p__5
-----------------------------
f(g(sk1))=sk1 \/ ~p__0 \/ ~p__5
*********** [45,60->61] ***********
~f(g(X0))=X0 \/ sk4=X0 \/ ~p__0
f(g(sk1))=sk1 \/ ~p__0 \/ ~p__5
-----------------------------
sk1=sk4 \/ ~p__0 \/ ~p__5
*********** [57,61->62] ***********
~sk1=sk4 \/ ~p__0 \/ ~p__5
sk1=sk4 \/ ~p__0 \/ ~p__5
-----------------------------
~p__5 \/ ~p__0
*********** [39,32,41,43->63] ***********
p__2 \/ ~p__0
~f(g(X0))=X0 \/ p__3
~f(g(X0))=X0 \/ ~f(g(X1))=X1 \/ X0=X1 \/ ~p__0
f(g(sk0))=sk0 \/ g(f(sk2))=sk2 \/ ~p__2 \/ ~p__3
-----------------------------
~f(g(X0))=X0 \/ sk0=X0 \/ p__5
*********** [62,38,63->64] ***********
~p__5 \/ ~p__0
f(g(sk4))=sk4 \/ ~p__0
~f(g(X0))=X0 \/ sk0=X0 \/ p__5
-----------------------------
sk0=sk4 \/ ~p__0
*********** [30,34,36,64->65] ***********
p__2
p__3
~sk0=sk1 \/ ~sk2=sk3 \/ ~p__2 \/ ~p__3
sk0=sk4 \/ ~p__0
-----------------------------
~sk1=sk4 \/ ~sk2=sk3 \/ ~p__0
*********** [11->14] ***********
(~X0=f(g(X0)) \/
((sk1=f(g(sk1)) &
~sk1=sk0) &
sk0=f(g(sk0))) \/
~X3=g(f(X3)) \/
((sk3=g(f(sk3)) &
~sk3=sk2) &
sk2=g(f(sk2)))) &
((sk4=f(g(sk4)) &
((~X8=f(g(X8)) \/
X8=X7) \/
~X7=f(g(X7)))) \/
(sk5=g(f(sk5)) &
((~X11=g(f(X11)) \/
X11=X10) \/
~X10=g(f(X10)))))
-----------------------------
sk2=g(f(sk2)) \/ ~X3=g(f(X3)) \/ sk1=f(g(sk1)) \/ ~X0=f(g(X0))
*********** [14->66] ***********
sk2=g(f(sk2)) \/ ~X3=g(f(X3)) \/ sk1=f(g(sk1)) \/ ~X0=f(g(X0))
-----------------------------
f(g(sk1))=sk1 \/ g(f(sk2))=sk2 \/ ~p__2 \/ ~p__3
*********** [66->67] ***********
f(g(sk1))=sk1 \/ g(f(sk2))=sk2 \/ ~p__2 \/ ~p__3
-----------------------------
f(g(sk1))=sk1 \/ g(f(sk2))=sk2 \/ ~p__2 \/ ~p__3
*********** [39,32,41,67->68] ***********
p__2 \/ ~p__0
~f(g(X0))=X0 \/ p__3
~f(g(X0))=X0 \/ ~f(g(X1))=X1 \/ X0=X1 \/ ~p__0
f(g(sk1))=sk1 \/ g(f(sk2))=sk2 \/ ~p__2 \/ ~p__3
-----------------------------
g(f(sk2))=sk2 \/ ~p__0 \/ ~p__7
*********** [68,45->69] ***********
g(f(sk2))=sk2 \/ ~p__0 \/ ~p__7
~f(g(X0))=X0 \/ sk4=X0 \/ ~p__0
-----------------------------
f(sk2)=sk4 \/ ~p__0 \/ ~p__7
*********** [68,69->70] ***********
g(f(sk2))=sk2 \/ ~p__0 \/ ~p__7
f(sk2)=sk4 \/ ~p__0 \/ ~p__7
-----------------------------
g(sk4)=sk2 \/ ~p__0 \/ ~p__7
*********** [11->12] ***********
(~X0=f(g(X0)) \/
((sk1=f(g(sk1)) &
~sk1=sk0) &
sk0=f(g(sk0))) \/
~X3=g(f(X3)) \/
((sk3=g(f(sk3)) &
~sk3=sk2) &
sk2=g(f(sk2)))) &
((sk4=f(g(sk4)) &
((~X8=f(g(X8)) \/
X8=X7) \/
~X7=f(g(X7)))) \/
(sk5=g(f(sk5)) &
((~X11=g(f(X11)) \/
X11=X10) \/
~X10=g(f(X10)))))
-----------------------------
sk3=g(f(sk3)) \/ ~X3=g(f(X3)) \/ sk1=f(g(sk1)) \/ ~X0=f(g(X0))
*********** [12->71] ***********
sk3=g(f(sk3)) \/ ~X3=g(f(X3)) \/ sk1=f(g(sk1)) \/ ~X0=f(g(X0))
-----------------------------
f(g(sk1))=sk1 \/ g(f(sk3))=sk3 \/ ~p__2 \/ ~p__3
*********** [71->72] ***********
f(g(sk1))=sk1 \/ g(f(sk3))=sk3 \/ ~p__2 \/ ~p__3
-----------------------------
f(g(sk1))=sk1 \/ g(f(sk3))=sk3 \/ ~p__2 \/ ~p__3
*********** [39,32,41,72->73] ***********
p__2 \/ ~p__0
~f(g(X0))=X0 \/ p__3
~f(g(X0))=X0 \/ ~f(g(X1))=X1 \/ X0=X1 \/ ~p__0
f(g(sk1))=sk1 \/ g(f(sk3))=sk3 \/ ~p__2 \/ ~p__3
-----------------------------
g(f(sk3))=sk3 \/ ~p__0 \/ ~p__7
*********** [73,45->74] ***********
g(f(sk3))=sk3 \/ ~p__0 \/ ~p__7
~f(g(X0))=X0 \/ sk4=X0 \/ ~p__0
-----------------------------
f(sk3)=sk4 \/ ~p__0 \/ ~p__7
*********** [70,73,74->75] ***********
g(sk4)=sk2 \/ ~p__0 \/ ~p__7
g(f(sk3))=sk3 \/ ~p__0 \/ ~p__7
f(sk3)=sk4 \/ ~p__0 \/ ~p__7
-----------------------------
sk2=sk3 \/ ~p__0 \/ ~p__7
*********** [30,34,54,75->76] ***********
p__2
p__3
~sk2=sk3 \/ f(g(sk0))=sk0 \/ ~p__2 \/ ~p__3
sk2=sk3 \/ ~p__0 \/ ~p__7
-----------------------------
f(g(sk0))=sk0 \/ ~p__0 \/ ~p__7
*********** [45,76->77] ***********
~f(g(X0))=X0 \/ sk4=X0 \/ ~p__0
f(g(sk0))=sk0 \/ ~p__0 \/ ~p__7
-----------------------------
sk0=sk4 \/ ~p__0 \/ ~p__7
*********** [75,30,34,36,77->78] ***********
sk2=sk3 \/ ~p__0 \/ ~p__7
p__2
p__3
~sk0=sk1 \/ ~sk2=sk3 \/ ~p__2 \/ ~p__3
sk0=sk4 \/ ~p__0 \/ ~p__7
-----------------------------
~sk1=sk4 \/ ~p__0 \/ ~p__7
*********** [30,34,59,75->79] ***********
p__2
p__3
~sk2=sk3 \/ f(g(sk1))=sk1 \/ ~p__2 \/ ~p__3
sk2=sk3 \/ ~p__0 \/ ~p__7
-----------------------------
f(g(sk1))=sk1 \/ ~p__0 \/ ~p__7
*********** [45,79->80] ***********
~f(g(X0))=X0 \/ sk4=X0 \/ ~p__0
f(g(sk1))=sk1 \/ ~p__0 \/ ~p__7
-----------------------------
sk1=sk4 \/ ~p__0 \/ ~p__7
*********** [78,80->81] ***********
~sk1=sk4 \/ ~p__0 \/ ~p__7
sk1=sk4 \/ ~p__0 \/ ~p__7
-----------------------------
~p__7 \/ ~p__0
*********** [39,32,41,67->82] ***********
p__2 \/ ~p__0
~f(g(X0))=X0 \/ p__3
~f(g(X0))=X0 \/ ~f(g(X1))=X1 \/ X0=X1 \/ ~p__0
f(g(sk1))=sk1 \/ g(f(sk2))=sk2 \/ ~p__2 \/ ~p__3
-----------------------------
~f(g(X0))=X0 \/ sk1=X0 \/ p__7
*********** [81,38,82->83] ***********
~p__7 \/ ~p__0
f(g(sk4))=sk4 \/ ~p__0
~f(g(X0))=X0 \/ sk1=X0 \/ p__7
-----------------------------
sk1=sk4 \/ ~p__0
*********** [65,83->84] ***********
~sk1=sk4 \/ ~sk2=sk3 \/ ~p__0
sk1=sk4 \/ ~p__0
-----------------------------
~sk2=sk3 \/ ~p__0
*********** [11->15] ***********
(~X0=f(g(X0)) \/
((sk1=f(g(sk1)) &
~sk1=sk0) &
sk0=f(g(sk0))) \/
~X3=g(f(X3)) \/
((sk3=g(f(sk3)) &
~sk3=sk2) &
sk2=g(f(sk2)))) &
((sk4=f(g(sk4)) &
((~X8=f(g(X8)) \/
X8=X7) \/
~X7=f(g(X7)))) \/
(sk5=g(f(sk5)) &
((~X11=g(f(X11)) \/
X11=X10) \/
~X10=g(f(X10)))))
-----------------------------
sk3=g(f(sk3)) \/ ~X3=g(f(X3)) \/ ~sk1=sk0 \/ ~X0=f(g(X0))
*********** [15->85] ***********
sk3=g(f(sk3)) \/ ~X3=g(f(X3)) \/ ~sk1=sk0 \/ ~X0=f(g(X0))
-----------------------------
~sk0=sk1 \/ g(f(sk3))=sk3 \/ ~p__2 \/ ~p__3
*********** [85->86] ***********
~sk0=sk1 \/ g(f(sk3))=sk3 \/ ~p__2 \/ ~p__3
-----------------------------
~sk0=sk1 \/ g(f(sk3))=sk3 \/ ~p__2 \/ ~p__3
*********** [30,34,86,64->87] ***********
p__2
p__3
~sk0=sk1 \/ g(f(sk3))=sk3 \/ ~p__2 \/ ~p__3
sk0=sk4 \/ ~p__0
-----------------------------
~sk1=sk4 \/ g(f(sk3))=sk3 \/ ~p__0
*********** [87,83->88] ***********
~sk1=sk4 \/ g(f(sk3))=sk3 \/ ~p__0
sk1=sk4 \/ ~p__0
-----------------------------
g(f(sk3))=sk3 \/ ~p__0
*********** [83,81,82,88->89] ***********
sk1=sk4 \/ ~p__0
~p__7 \/ ~p__0
~f(g(X0))=X0 \/ sk1=X0 \/ p__7
g(f(sk3))=sk3 \/ ~p__0
-----------------------------
f(sk3)=sk4 \/ ~p__0
*********** [88,89->90] ***********
g(f(sk3))=sk3 \/ ~p__0
f(sk3)=sk4 \/ ~p__0
-----------------------------
g(sk4)=sk3 \/ ~p__0
*********** [11->17] ***********
(~X0=f(g(X0)) \/
((sk1=f(g(sk1)) &
~sk1=sk0) &
sk0=f(g(sk0))) \/
~X3=g(f(X3)) \/
((sk3=g(f(sk3)) &
~sk3=sk2) &
sk2=g(f(sk2)))) &
((sk4=f(g(sk4)) &
((~X8=f(g(X8)) \/
X8=X7) \/
~X7=f(g(X7)))) \/
(sk5=g(f(sk5)) &
((~X11=g(f(X11)) \/
X11=X10) \/
~X10=g(f(X10)))))
-----------------------------
sk2=g(f(sk2)) \/ ~X3=g(f(X3)) \/ ~sk1=sk0 \/ ~X0=f(g(X0))
*********** [17->91] ***********
sk2=g(f(sk2)) \/ ~X3=g(f(X3)) \/ ~sk1=sk0 \/ ~X0=f(g(X0))
-----------------------------
~sk0=sk1 \/ g(f(sk2))=sk2 \/ ~p__2 \/ ~p__3
*********** [91->92] ***********
~sk0=sk1 \/ g(f(sk2))=sk2 \/ ~p__2 \/ ~p__3
-----------------------------
~sk0=sk1 \/ g(f(sk2))=sk2 \/ ~p__2 \/ ~p__3
*********** [30,34,92,64->93] ***********
p__2
p__3
~sk0=sk1 \/ g(f(sk2))=sk2 \/ ~p__2 \/ ~p__3
sk0=sk4 \/ ~p__0
-----------------------------
~sk1=sk4 \/ g(f(sk2))=sk2 \/ ~p__0
*********** [93,83->94] ***********
~sk1=sk4 \/ g(f(sk2))=sk2 \/ ~p__0
sk1=sk4 \/ ~p__0
-----------------------------
g(f(sk2))=sk2 \/ ~p__0
*********** [83,81,82,94->95] ***********
sk1=sk4 \/ ~p__0
~p__7 \/ ~p__0
~f(g(X0))=X0 \/ sk1=X0 \/ p__7
g(f(sk2))=sk2 \/ ~p__0
-----------------------------
f(sk2)=sk4 \/ ~p__0
*********** [90,94,95->96] ***********
g(sk4)=sk3 \/ ~p__0
g(f(sk2))=sk2 \/ ~p__0
f(sk2)=sk4 \/ ~p__0
-----------------------------
sk2=sk3 \/ ~p__0
*********** [84,96->97] ***********
~sk2=sk3 \/ ~p__0
sk2=sk3 \/ ~p__0
-----------------------------
~p__0
*********** [11->23] ***********
(~X0=f(g(X0)) \/
((sk1=f(g(sk1)) &
~sk1=sk0) &
sk0=f(g(sk0))) \/
~X3=g(f(X3)) \/
((sk3=g(f(sk3)) &
~sk3=sk2) &
sk2=g(f(sk2)))) &
((sk4=f(g(sk4)) &
((~X8=f(g(X8)) \/
X8=X7) \/
~X7=f(g(X7)))) \/
(sk5=g(f(sk5)) &
((~X11=g(f(X11)) \/
X11=X10) \/
~X10=g(f(X10)))))
-----------------------------
sk5=g(f(sk5)) \/ ~X7=f(g(X7)) \/ X8=X7 \/ ~X8=f(g(X8))
*********** [23->98] ***********
sk5=g(f(sk5)) \/ ~X7=f(g(X7)) \/ X8=X7 \/ ~X8=f(g(X8))
-----------------------------
g(f(sk5))=sk5 \/ p__1
*********** [98->99] ***********
g(f(sk5))=sk5 \/ p__1
-----------------------------
g(f(sk5))=sk5 \/ p__1
*********** [23->100] ***********
sk5=g(f(sk5)) \/ ~X7=f(g(X7)) \/ X8=X7 \/ ~X8=f(g(X8))
-----------------------------
~f(g(X0))=X0 \/ ~f(g(X1))=X1 \/ X0=X1 \/ ~p__1
*********** [100->101] ***********
~f(g(X0))=X0 \/ ~f(g(X1))=X1 \/ X0=X1 \/ ~p__1
-----------------------------
~f(g(X0))=X0 \/ ~f(g(X1))=X1 \/ X0=X1 \/ ~p__1
*********** [99,101,28->102] ***********
g(f(sk5))=sk5 \/ p__1
~f(g(X0))=X0 \/ ~f(g(X1))=X1 \/ X0=X1 \/ ~p__1
f(g(sk4))=sk4 \/ g(f(sk5))=sk5
-----------------------------
~f(g(X0))=X0 \/ sk4=X0 \/ ~p__1
*********** [32,101,67->103] ***********
~f(g(X0))=X0 \/ p__3
~f(g(X0))=X0 \/ ~f(g(X1))=X1 \/ X0=X1 \/ ~p__1
f(g(sk1))=sk1 \/ g(f(sk2))=sk2 \/ ~p__2 \/ ~p__3
-----------------------------
g(f(sk2))=sk2 \/ ~p__1 \/ ~p__2 \/ ~p__7
*********** [30,102,103->104] ***********
p__2
~f(g(X0))=X0 \/ sk4=X0 \/ ~p__1
g(f(sk2))=sk2 \/ ~p__1 \/ ~p__2 \/ ~p__7
-----------------------------
f(sk2)=sk4 \/ ~p__1 \/ ~p__7
*********** [24->105] ***********
~X10=g(f(X10)) \/ X11=X10 \/ ~X11=g(f(X11)) \/ ~X7=f(g(X7)) \/ X8=X7 \/ ~X8=f(g(X8))
-----------------------------
~g(f(X0))=X0 \/ ~g(f(X1))=X1 \/ X0=X1 \/ p__0
*********** [105->106] ***********
~g(f(X0))=X0 \/ ~g(f(X1))=X1 \/ X0=X1 \/ p__0
-----------------------------
~g(f(X0))=X0 \/ ~g(f(X1))=X1 \/ X0=X1 \/ p__0
*********** [106,28->107] ***********
~g(f(X0))=X0 \/ ~g(f(X1))=X1 \/ X0=X1 \/ p__0
f(g(sk4))=sk4 \/ g(f(sk5))=sk5
-----------------------------
~g(f(X0))=X0 \/ g(sk4)=X0 \/ p__0 \/ ~p__1
*********** [26,106,67->108] ***********
~g(f(X0))=X0 \/ p__2
~g(f(X0))=X0 \/ ~g(f(X1))=X1 \/ X0=X1 \/ p__0
f(g(sk1))=sk1 \/ g(f(sk2))=sk2 \/ ~p__2 \/ ~p__3
-----------------------------
g(f(sk2))=sk2 \/ p__0 \/ ~p__3 \/ ~p__6
*********** [34,107,108->109] ***********
p__3
~g(f(X0))=X0 \/ g(sk4)=X0 \/ p__0 \/ ~p__1
g(f(sk2))=sk2 \/ p__0 \/ ~p__3 \/ ~p__6
-----------------------------
g(sk4)=sk2 \/ p__0 \/ ~p__1 \/ ~p__6
*********** [26,106,72->110] ***********
~g(f(X0))=X0 \/ p__2
~g(f(X0))=X0 \/ ~g(f(X1))=X1 \/ X0=X1 \/ p__0
f(g(sk1))=sk1 \/ g(f(sk3))=sk3 \/ ~p__2 \/ ~p__3
-----------------------------
g(f(sk3))=sk3 \/ p__0 \/ ~p__3 \/ ~p__6
*********** [97,34,107,110->111] ***********
~p__0
p__3
~g(f(X0))=X0 \/ g(sk4)=X0 \/ p__0 \/ ~p__1
g(f(sk3))=sk3 \/ p__0 \/ ~p__3 \/ ~p__6
-----------------------------
g(sk4)=sk3 \/ ~p__1 \/ ~p__6
*********** [97,109,111->112] ***********
~p__0
g(sk4)=sk2 \/ p__0 \/ ~p__1 \/ ~p__6
g(sk4)=sk3 \/ ~p__1 \/ ~p__6
-----------------------------
sk2=sk3 \/ ~p__1 \/ ~p__6
*********** [26,106,67->113] ***********
~g(f(X0))=X0 \/ p__2
~g(f(X0))=X0 \/ ~g(f(X1))=X1 \/ X0=X1 \/ p__0
f(g(sk1))=sk1 \/ g(f(sk2))=sk2 \/ ~p__2 \/ ~p__3
-----------------------------
~g(f(X0))=X0 \/ g(sk1)=X0 \/ p__6
*********** [30,113,103->114] ***********
p__2
~g(f(X0))=X0 \/ g(sk1)=X0 \/ p__6
g(f(sk2))=sk2 \/ ~p__1 \/ ~p__2 \/ ~p__7
-----------------------------
g(sk1)=sk2 \/ ~p__1 \/ p__6 \/ ~p__7
*********** [32,101,72->115] ***********
~f(g(X0))=X0 \/ p__3
~f(g(X0))=X0 \/ ~f(g(X1))=X1 \/ X0=X1 \/ ~p__1
f(g(sk1))=sk1 \/ g(f(sk3))=sk3 \/ ~p__2 \/ ~p__3
-----------------------------
g(f(sk3))=sk3 \/ ~p__1 \/ ~p__2 \/ ~p__7
*********** [112,114,30,113,115->116] ***********
sk2=sk3 \/ ~p__1 \/ ~p__6
g(sk1)=sk2 \/ ~p__1 \/ p__6 \/ ~p__7
p__2
~g(f(X0))=X0 \/ g(sk1)=X0 \/ p__6
g(f(sk3))=sk3 \/ ~p__1 \/ ~p__2 \/ ~p__7
-----------------------------
sk2=sk3 \/ ~p__1 \/ ~p__7
*********** [104,116->117] ***********
f(sk2)=sk4 \/ ~p__1 \/ ~p__7
sk2=sk3 \/ ~p__1 \/ ~p__7
-----------------------------
f(sk3)=sk4 \/ ~p__1 \/ ~p__7
*********** [106,99->118] ***********
~g(f(X0))=X0 \/ ~g(f(X1))=X1 \/ X0=X1 \/ p__0
g(f(sk5))=sk5 \/ p__1
-----------------------------
~g(f(X0))=X0 \/ sk5=X0 \/ p__0 \/ p__1
*********** [26,106,43->119] ***********
~g(f(X0))=X0 \/ p__2
~g(f(X0))=X0 \/ ~g(f(X1))=X1 \/ X0=X1 \/ p__0
f(g(sk0))=sk0 \/ g(f(sk2))=sk2 \/ ~p__2 \/ ~p__3
-----------------------------
g(f(sk2))=sk2 \/ p__0 \/ ~p__3 \/ ~p__4
*********** [34,118,119->120] ***********
p__3
~g(f(X0))=X0 \/ sk5=X0 \/ p__0 \/ p__1
g(f(sk2))=sk2 \/ p__0 \/ ~p__3 \/ ~p__4
-----------------------------
sk2=sk5 \/ p__0 \/ p__1 \/ ~p__4
*********** [30,34,54,120->121] ***********
p__2
p__3
~sk2=sk3 \/ f(g(sk0))=sk0 \/ ~p__2 \/ ~p__3
sk2=sk5 \/ p__0 \/ p__1 \/ ~p__4
-----------------------------
~sk3=sk5 \/ f(g(sk0))=sk0 \/ p__0 \/ p__1 \/ ~p__4
*********** [26,106,49->122] ***********
~g(f(X0))=X0 \/ p__2
~g(f(X0))=X0 \/ ~g(f(X1))=X1 \/ X0=X1 \/ p__0
f(g(sk0))=sk0 \/ g(f(sk3))=sk3 \/ ~p__2 \/ ~p__3
-----------------------------
g(f(sk3))=sk3 \/ p__0 \/ ~p__3 \/ ~p__4
*********** [34,118,122->123] ***********
p__3
~g(f(X0))=X0 \/ sk5=X0 \/ p__0 \/ p__1
g(f(sk3))=sk3 \/ p__0 \/ ~p__3 \/ ~p__4
-----------------------------
sk3=sk5 \/ p__0 \/ p__1 \/ ~p__4
*********** [121,123->124] ***********
~sk3=sk5 \/ f(g(sk0))=sk0 \/ p__0 \/ p__1 \/ ~p__4
sk3=sk5 \/ p__0 \/ p__1 \/ ~p__4
-----------------------------
f(g(sk0))=sk0 \/ p__0 \/ p__1 \/ ~p__4
*********** [34,107,119->125] ***********
p__3
~g(f(X0))=X0 \/ g(sk4)=X0 \/ p__0 \/ ~p__1
g(f(sk2))=sk2 \/ p__0 \/ ~p__3 \/ ~p__4
-----------------------------
g(sk4)=sk2 \/ p__0 \/ ~p__1 \/ ~p__4
*********** [125,34,107,122->126] ***********
g(sk4)=sk2 \/ p__0 \/ ~p__1 \/ ~p__4
p__3
~g(f(X0))=X0 \/ g(sk4)=X0 \/ p__0 \/ ~p__1
g(f(sk3))=sk3 \/ p__0 \/ ~p__3 \/ ~p__4
-----------------------------
sk2=sk3 \/ p__0 \/ ~p__1 \/ ~p__4
*********** [30,34,124,54,126->127] ***********
p__2
p__3
f(g(sk0))=sk0 \/ p__0 \/ p__1 \/ ~p__4
~sk2=sk3 \/ f(g(sk0))=sk0 \/ ~p__2 \/ ~p__3
sk2=sk3 \/ p__0 \/ ~p__1 \/ ~p__4
-----------------------------
f(g(sk0))=sk0 \/ p__0 \/ ~p__4
*********** [64,102,127->128] ***********
sk0=sk4 \/ ~p__0
~f(g(X0))=X0 \/ sk4=X0 \/ ~p__1
f(g(sk0))=sk0 \/ p__0 \/ ~p__4
-----------------------------
sk0=sk4 \/ ~p__1 \/ ~p__4
*********** [34,102,108->129] ***********
p__3
~f(g(X0))=X0 \/ sk4=X0 \/ ~p__1
g(f(sk2))=sk2 \/ p__0 \/ ~p__3 \/ ~p__6
-----------------------------
f(sk2)=sk4 \/ p__0 \/ ~p__1 \/ ~p__6
*********** [97,129,112->130] ***********
~p__0
f(sk2)=sk4 \/ p__0 \/ ~p__1 \/ ~p__6
sk2=sk3 \/ ~p__1 \/ ~p__6
-----------------------------
f(sk3)=sk4 \/ ~p__1 \/ ~p__6
*********** [26,106,43->131] ***********
~g(f(X0))=X0 \/ p__2
~g(f(X0))=X0 \/ ~g(f(X1))=X1 \/ X0=X1 \/ p__0
f(g(sk0))=sk0 \/ g(f(sk2))=sk2 \/ ~p__2 \/ ~p__3
-----------------------------
~g(f(X0))=X0 \/ g(sk0)=X0 \/ p__4
*********** [97,34,131,110->132] ***********
~p__0
p__3
~g(f(X0))=X0 \/ g(sk0)=X0 \/ p__4
g(f(sk3))=sk3 \/ p__0 \/ ~p__3 \/ ~p__6
-----------------------------
g(sk0)=sk3 \/ p__4 \/ ~p__6
*********** [34,131,108->133] ***********
p__3
~g(f(X0))=X0 \/ g(sk0)=X0 \/ p__4
g(f(sk2))=sk2 \/ p__0 \/ ~p__3 \/ ~p__6
-----------------------------
g(sk0)=sk2 \/ p__0 \/ p__4 \/ ~p__6
*********** [97,133,132->134] ***********
~p__0
g(sk0)=sk2 \/ p__0 \/ p__4 \/ ~p__6
g(sk0)=sk3 \/ p__4 \/ ~p__6
-----------------------------
sk2=sk3 \/ p__4 \/ ~p__6
*********** [132,30,34,54,134->135] ***********
g(sk0)=sk3 \/ p__4 \/ ~p__6
p__2
p__3
~sk2=sk3 \/ f(g(sk0))=sk0 \/ ~p__2 \/ ~p__3
sk2=sk3 \/ p__4 \/ ~p__6
-----------------------------
f(sk3)=sk0 \/ p__4 \/ ~p__6
*********** [128,130,135->136] ***********
sk0=sk4 \/ ~p__1 \/ ~p__4
f(sk3)=sk4 \/ ~p__1 \/ ~p__6
f(sk3)=sk0 \/ p__4 \/ ~p__6
-----------------------------
sk0=sk4 \/ ~p__1 \/ ~p__6
*********** [112,30,34,36,136->137] ***********
sk2=sk3 \/ ~p__1 \/ ~p__6
p__2
p__3
~sk0=sk1 \/ ~sk2=sk3 \/ ~p__2 \/ ~p__3
sk0=sk4 \/ ~p__1 \/ ~p__6
-----------------------------
~sk1=sk4 \/ ~p__1 \/ ~p__6
*********** [34,118,108->138] ***********
p__3
~g(f(X0))=X0 \/ sk5=X0 \/ p__0 \/ p__1
g(f(sk2))=sk2 \/ p__0 \/ ~p__3 \/ ~p__6
-----------------------------
sk2=sk5 \/ p__0 \/ p__1 \/ ~p__6
*********** [30,34,59,138->139] ***********
p__2
p__3
~sk2=sk3 \/ f(g(sk1))=sk1 \/ ~p__2 \/ ~p__3
sk2=sk5 \/ p__0 \/ p__1 \/ ~p__6
-----------------------------
~sk3=sk5 \/ f(g(sk1))=sk1 \/ p__0 \/ p__1 \/ ~p__6
*********** [97,34,118,110->140] ***********
~p__0
p__3
~g(f(X0))=X0 \/ sk5=X0 \/ p__0 \/ p__1
g(f(sk3))=sk3 \/ p__0 \/ ~p__3 \/ ~p__6
-----------------------------
sk3=sk5 \/ p__1 \/ ~p__6
*********** [97,139,140->141] ***********
~p__0
~sk3=sk5 \/ f(g(sk1))=sk1 \/ p__0 \/ p__1 \/ ~p__6
sk3=sk5 \/ p__1 \/ ~p__6
-----------------------------
f(g(sk1))=sk1 \/ p__1 \/ ~p__6
*********** [30,34,141,59,112->142] ***********
p__2
p__3
f(g(sk1))=sk1 \/ p__1 \/ ~p__6
~sk2=sk3 \/ f(g(sk1))=sk1 \/ ~p__2 \/ ~p__3
sk2=sk3 \/ ~p__1 \/ ~p__6
-----------------------------
f(g(sk1))=sk1 \/ ~p__6
*********** [102,142->143] ***********
~f(g(X0))=X0 \/ sk4=X0 \/ ~p__1
f(g(sk1))=sk1 \/ ~p__6
-----------------------------
sk1=sk4 \/ ~p__1 \/ ~p__6
*********** [137,143->144] ***********
~sk1=sk4 \/ ~p__1 \/ ~p__6
sk1=sk4 \/ ~p__1 \/ ~p__6
-----------------------------
~p__6 \/ ~p__1
*********** [30,34,54,138->145] ***********
p__2
p__3
~sk2=sk3 \/ f(g(sk0))=sk0 \/ ~p__2 \/ ~p__3
sk2=sk5 \/ p__0 \/ p__1 \/ ~p__6
-----------------------------
~sk3=sk5 \/ f(g(sk0))=sk0 \/ p__0 \/ p__1 \/ ~p__6
*********** [99,131->146] ***********
g(f(sk5))=sk5 \/ p__1
~g(f(X0))=X0 \/ g(sk0)=X0 \/ p__4
-----------------------------
g(sk0)=sk5 \/ p__1 \/ p__4
*********** [146,118,127->147] ***********
g(sk0)=sk5 \/ p__1 \/ p__4
~g(f(X0))=X0 \/ sk5=X0 \/ p__0 \/ p__1
f(g(sk0))=sk0 \/ p__0 \/ ~p__4
-----------------------------
g(sk0)=sk5 \/ p__0 \/ p__1
*********** [145,147->148] ***********
~sk3=sk5 \/ f(g(sk0))=sk0 \/ p__0 \/ p__1 \/ ~p__6
g(sk0)=sk5 \/ p__0 \/ p__1
-----------------------------
~sk3=sk5 \/ f(sk5)=sk0 \/ p__0 \/ p__1 \/ ~p__6
*********** [97,148,140->149] ***********
~p__0
~sk3=sk5 \/ f(sk5)=sk0 \/ p__0 \/ p__1 \/ ~p__6
sk3=sk5 \/ p__1 \/ ~p__6
-----------------------------
f(sk5)=sk0 \/ p__1 \/ ~p__6
*********** [99,113->150] ***********
g(f(sk5))=sk5 \/ p__1
~g(f(X0))=X0 \/ g(sk1)=X0 \/ p__6
-----------------------------
g(sk1)=sk5 \/ p__1 \/ p__6
*********** [97,150,118,142->151] ***********
~p__0
g(sk1)=sk5 \/ p__1 \/ p__6
~g(f(X0))=X0 \/ sk5=X0 \/ p__0 \/ p__1
f(g(sk1))=sk1 \/ ~p__6
-----------------------------
g(sk1)=sk5 \/ p__1
*********** [144,142,151->152] ***********
~p__6 \/ ~p__1
f(g(sk1))=sk1 \/ ~p__6
g(sk1)=sk5 \/ p__1
-----------------------------
f(sk5)=sk1 \/ ~p__6
*********** [144,149,152->153] ***********
~p__6 \/ ~p__1
f(sk5)=sk0 \/ p__1 \/ ~p__6
f(sk5)=sk1 \/ ~p__6
-----------------------------
sk0=sk1 \/ ~p__6
*********** [30,34,36,153->154] ***********
p__2
p__3
~sk0=sk1 \/ ~sk2=sk3 \/ ~p__2 \/ ~p__3
sk0=sk1 \/ ~p__6
-----------------------------
~sk2=sk3 \/ ~p__6
*********** [97,144,138,154->155] ***********
~p__0
~p__6 \/ ~p__1
sk2=sk5 \/ p__0 \/ p__1 \/ ~p__6
~sk2=sk3 \/ ~p__6
-----------------------------
~sk3=sk5 \/ ~p__6
*********** [144,140,155->156] ***********
~p__6 \/ ~p__1
sk3=sk5 \/ p__1 \/ ~p__6
~sk3=sk5 \/ ~p__6
-----------------------------
~p__6
*********** [114,116->157] ***********
g(sk1)=sk2 \/ ~p__1 \/ p__6 \/ ~p__7
sk2=sk3 \/ ~p__1 \/ ~p__7
-----------------------------
g(sk1)=sk3 \/ ~p__1 \/ p__6 \/ ~p__7
*********** [156,82,101,157->158] ***********
~p__6
~f(g(X0))=X0 \/ sk1=X0 \/ p__7
~f(g(X0))=X0 \/ ~f(g(X1))=X1 \/ X0=X1 \/ ~p__1
g(sk1)=sk3 \/ ~p__1 \/ p__6 \/ ~p__7
-----------------------------
~f(sk3)=sk1 \/ ~p__1 \/ ~p__7
*********** [117,158->159] ***********
f(sk3)=sk4 \/ ~p__1 \/ ~p__7
~f(sk3)=sk1 \/ ~p__1 \/ ~p__7
-----------------------------
~sk1=sk4 \/ ~p__1 \/ ~p__7
*********** [30,34,59,116->160] ***********
p__2
p__3
~sk2=sk3 \/ f(g(sk1))=sk1 \/ ~p__2 \/ ~p__3
sk2=sk3 \/ ~p__1 \/ ~p__7
-----------------------------
f(g(sk1))=sk1 \/ ~p__1 \/ ~p__7
*********** [117,156,157,160->161] ***********
f(sk3)=sk4 \/ ~p__1 \/ ~p__7
~p__6
g(sk1)=sk3 \/ ~p__1 \/ p__6 \/ ~p__7
f(g(sk1))=sk1 \/ ~p__1 \/ ~p__7
-----------------------------
sk1=sk4 \/ ~p__1 \/ ~p__7
*********** [159,161->162] ***********
~sk1=sk4 \/ ~p__1 \/ ~p__7
sk1=sk4 \/ ~p__1 \/ ~p__7
-----------------------------
~p__7 \/ ~p__1
*********** [28,82->163] ***********
f(g(sk4))=sk4 \/ g(f(sk5))=sk5
~f(g(X0))=X0 \/ sk1=X0 \/ p__7
-----------------------------
g(f(sk5))=sk5 \/ sk1=sk4 \/ p__7
*********** [82,163->164] ***********
~f(g(X0))=X0 \/ sk1=X0 \/ p__7
g(f(sk5))=sk5 \/ sk1=sk4 \/ p__7
-----------------------------
f(sk5)=sk1 \/ sk1=sk4 \/ p__7
*********** [162,102,163->165] ***********
~p__7 \/ ~p__1
~f(g(X0))=X0 \/ sk4=X0 \/ ~p__1
g(f(sk5))=sk5 \/ sk1=sk4 \/ p__7
-----------------------------
f(sk5)=sk4 \/ sk1=sk4 \/ ~p__1
*********** [162,164,165->166] ***********
~p__7 \/ ~p__1
f(sk5)=sk1 \/ sk1=sk4 \/ p__7
f(sk5)=sk4 \/ sk1=sk4 \/ ~p__1
-----------------------------
sk1=sk4 \/ ~p__1
*********** [32,101,43->167] ***********
~f(g(X0))=X0 \/ p__3
~f(g(X0))=X0 \/ ~f(g(X1))=X1 \/ X0=X1 \/ ~p__1
f(g(sk0))=sk0 \/ g(f(sk2))=sk2 \/ ~p__2 \/ ~p__3
-----------------------------
g(f(sk2))=sk2 \/ ~p__1 \/ ~p__2 \/ ~p__5
*********** [30,102,167->168] ***********
p__2
~f(g(X0))=X0 \/ sk4=X0 \/ ~p__1
g(f(sk2))=sk2 \/ ~p__1 \/ ~p__2 \/ ~p__5
-----------------------------
f(sk2)=sk4 \/ ~p__1 \/ ~p__5
*********** [62,30,107,167->169] ***********
~p__5 \/ ~p__0
p__2
~g(f(X0))=X0 \/ g(sk4)=X0 \/ p__0 \/ ~p__1
g(f(sk2))=sk2 \/ ~p__1 \/ ~p__2 \/ ~p__5
-----------------------------
g(sk4)=sk2 \/ ~p__1 \/ ~p__5
*********** [32,101,49->170] ***********
~f(g(X0))=X0 \/ p__3
~f(g(X0))=X0 \/ ~f(g(X1))=X1 \/ X0=X1 \/ ~p__1
f(g(sk0))=sk0 \/ g(f(sk3))=sk3 \/ ~p__2 \/ ~p__3
-----------------------------
g(f(sk3))=sk3 \/ ~p__1 \/ ~p__2 \/ ~p__5
*********** [169,62,30,107,170->171] ***********
g(sk4)=sk2 \/ ~p__1 \/ ~p__5
~p__5 \/ ~p__0
p__2
~g(f(X0))=X0 \/ g(sk4)=X0 \/ p__0 \/ ~p__1
g(f(sk3))=sk3 \/ ~p__1 \/ ~p__2 \/ ~p__5
-----------------------------
sk2=sk3 \/ ~p__1 \/ ~p__5
*********** [168,171->172] ***********
f(sk2)=sk4 \/ ~p__1 \/ ~p__5
sk2=sk3 \/ ~p__1 \/ ~p__5
-----------------------------
f(sk3)=sk4 \/ ~p__1 \/ ~p__5
*********** [34,119,113->173] ***********
p__3
g(f(sk2))=sk2 \/ p__0 \/ ~p__3 \/ ~p__4
~g(f(X0))=X0 \/ g(sk1)=X0 \/ p__6
-----------------------------
g(sk1)=sk2 \/ p__0 \/ ~p__4 \/ p__6
*********** [173,34,122,113->174] ***********
g(sk1)=sk2 \/ p__0 \/ ~p__4 \/ p__6
p__3
g(f(sk3))=sk3 \/ p__0 \/ ~p__3 \/ ~p__4
~g(f(X0))=X0 \/ g(sk1)=X0 \/ p__6
-----------------------------
sk2=sk3 \/ p__0 \/ ~p__4 \/ p__6
*********** [30,34,36,128->175] ***********
p__2
p__3
~sk0=sk1 \/ ~sk2=sk3 \/ ~p__2 \/ ~p__3
sk0=sk4 \/ ~p__1 \/ ~p__4
-----------------------------
~sk1=sk4 \/ ~sk2=sk3 \/ ~p__1 \/ ~p__4
*********** [30,34,59,120->176] ***********
p__2
p__3
~sk2=sk3 \/ f(g(sk1))=sk1 \/ ~p__2 \/ ~p__3
sk2=sk5 \/ p__0 \/ p__1 \/ ~p__4
-----------------------------
~sk3=sk5 \/ f(g(sk1))=sk1 \/ p__0 \/ p__1 \/ ~p__4
*********** [176,123->177] ***********
~sk3=sk5 \/ f(g(sk1))=sk1 \/ p__0 \/ p__1 \/ ~p__4
sk3=sk5 \/ p__0 \/ p__1 \/ ~p__4
-----------------------------
f(g(sk1))=sk1 \/ p__0 \/ p__1 \/ ~p__4
*********** [30,34,177,59,126->178] ***********
p__2
p__3
f(g(sk1))=sk1 \/ p__0 \/ p__1 \/ ~p__4
~sk2=sk3 \/ f(g(sk1))=sk1 \/ ~p__2 \/ ~p__3
sk2=sk3 \/ p__0 \/ ~p__1 \/ ~p__4
-----------------------------
f(g(sk1))=sk1 \/ p__0 \/ ~p__4
*********** [97,102,178->179] ***********
~p__0
~f(g(X0))=X0 \/ sk4=X0 \/ ~p__1
f(g(sk1))=sk1 \/ p__0 \/ ~p__4
-----------------------------
sk1=sk4 \/ ~p__1 \/ ~p__4
*********** [175,179->180] ***********
~sk1=sk4 \/ ~sk2=sk3 \/ ~p__1 \/ ~p__4
sk1=sk4 \/ ~p__1 \/ ~p__4
-----------------------------
~sk2=sk3 \/ ~p__1 \/ ~p__4
*********** [127,147->181] ***********
f(g(sk0))=sk0 \/ p__0 \/ ~p__4
g(sk0)=sk5 \/ p__0 \/ p__1
-----------------------------
f(sk5)=sk0 \/ p__0 \/ p__1 \/ ~p__4
*********** [97,151,178->182] ***********
~p__0
g(sk1)=sk5 \/ p__1
f(g(sk1))=sk1 \/ p__0 \/ ~p__4
-----------------------------
f(sk5)=sk1 \/ p__1 \/ ~p__4
*********** [97,181,182->183] ***********
~p__0
f(sk5)=sk0 \/ p__0 \/ p__1 \/ ~p__4
f(sk5)=sk1 \/ p__1 \/ ~p__4
-----------------------------
sk0=sk1 \/ p__1 \/ ~p__4
*********** [30,34,180,36,183->184] ***********
p__2
p__3
~sk2=sk3 \/ ~p__1 \/ ~p__4
~sk0=sk1 \/ ~sk2=sk3 \/ ~p__2 \/ ~p__3
sk0=sk1 \/ p__1 \/ ~p__4
-----------------------------
~sk2=sk3 \/ ~p__4
*********** [97,156,174,184->185] ***********
~p__0
~p__6
sk2=sk3 \/ p__0 \/ ~p__4 \/ p__6
~sk2=sk3 \/ ~p__4
-----------------------------
~p__4
*********** [30,131,167->186] ***********
p__2
~g(f(X0))=X0 \/ g(sk0)=X0 \/ p__4
g(f(sk2))=sk2 \/ ~p__1 \/ ~p__2 \/ ~p__5
-----------------------------
g(sk0)=sk2 \/ ~p__1 \/ p__4 \/ ~p__5
*********** [186,30,131,170->187] ***********
g(sk0)=sk2 \/ ~p__1 \/ p__4 \/ ~p__5
p__2
~g(f(X0))=X0 \/ g(sk0)=X0 \/ p__4
g(f(sk3))=sk3 \/ ~p__1 \/ ~p__2 \/ ~p__5
-----------------------------
sk2=sk3 \/ ~p__1 \/ p__4 \/ ~p__5
*********** [186,187->188] ***********
g(sk0)=sk2 \/ ~p__1 \/ p__4 \/ ~p__5
sk2=sk3 \/ ~p__1 \/ p__4 \/ ~p__5
-----------------------------
g(sk0)=sk3 \/ ~p__1 \/ p__4 \/ ~p__5
*********** [185,63,101,188->189] ***********
~p__4
~f(g(X0))=X0 \/ sk0=X0 \/ p__5
~f(g(X0))=X0 \/ ~f(g(X1))=X1 \/ X0=X1 \/ ~p__1
g(sk0)=sk3 \/ ~p__1 \/ p__4 \/ ~p__5
-----------------------------
~f(sk3)=sk0 \/ ~p__1 \/ ~p__5
*********** [172,189->190] ***********
f(sk3)=sk4 \/ ~p__1 \/ ~p__5
~f(sk3)=sk0 \/ ~p__1 \/ ~p__5
-----------------------------
~sk0=sk4 \/ ~p__1 \/ ~p__5
*********** [30,34,54,171->191] ***********
p__2
p__3
~sk2=sk3 \/ f(g(sk0))=sk0 \/ ~p__2 \/ ~p__3
sk2=sk3 \/ ~p__1 \/ ~p__5
-----------------------------
f(g(sk0))=sk0 \/ ~p__1 \/ ~p__5
*********** [172,185,188,191->192] ***********
f(sk3)=sk4 \/ ~p__1 \/ ~p__5
~p__4
g(sk0)=sk3 \/ ~p__1 \/ p__4 \/ ~p__5
f(g(sk0))=sk0 \/ ~p__1 \/ ~p__5
-----------------------------
sk0=sk4 \/ ~p__1 \/ ~p__5
*********** [190,192->193] ***********
~sk0=sk4 \/ ~p__1 \/ ~p__5
sk0=sk4 \/ ~p__1 \/ ~p__5
-----------------------------
~p__5 \/ ~p__1
*********** [30,34,49,102->194] ***********
p__2
p__3
f(g(sk0))=sk0 \/ g(f(sk3))=sk3 \/ ~p__2 \/ ~p__3
~f(g(X0))=X0 \/ sk4=X0 \/ ~p__1
-----------------------------
g(f(sk3))=sk3 \/ sk0=sk4 \/ ~p__1
*********** [102,194->195] ***********
~f(g(X0))=X0 \/ sk4=X0 \/ ~p__1
g(f(sk3))=sk3 \/ sk0=sk4 \/ ~p__1
-----------------------------
f(sk3)=sk4 \/ sk0=sk4 \/ ~p__1
*********** [30,34,72,63->196] ***********
p__2
p__3
f(g(sk1))=sk1 \/ g(f(sk3))=sk3 \/ ~p__2 \/ ~p__3
~f(g(X0))=X0 \/ sk0=X0 \/ p__5
-----------------------------
g(f(sk3))=sk3 \/ sk0=sk1 \/ p__5
*********** [63,196->197] ***********
~f(g(X0))=X0 \/ sk0=X0 \/ p__5
g(f(sk3))=sk3 \/ sk0=sk1 \/ p__5
-----------------------------
f(sk3)=sk0 \/ sk0=sk1 \/ p__5
*********** [193,195,197->198] ***********
~p__5 \/ ~p__1
f(sk3)=sk4 \/ sk0=sk4 \/ ~p__1
f(sk3)=sk0 \/ sk0=sk1 \/ p__5
-----------------------------
sk0=sk1 \/ sk0=sk4 \/ ~p__1
*********** [198,166->199] ***********
sk0=sk1 \/ sk0=sk4 \/ ~p__1
sk1=sk4 \/ ~p__1
-----------------------------
sk0=sk4 \/ ~p__1
*********** [166,30,34,36,199->200] ***********
sk1=sk4 \/ ~p__1
p__2
p__3
~sk0=sk1 \/ ~sk2=sk3 \/ ~p__2 \/ ~p__3
sk0=sk4 \/ ~p__1
-----------------------------
~sk2=sk3 \/ ~p__1
*********** [97,106,194->201] ***********
~p__0
~g(f(X0))=X0 \/ ~g(f(X1))=X1 \/ X0=X1 \/ p__0
g(f(sk3))=sk3 \/ sk0=sk4 \/ ~p__1
-----------------------------
sk0=sk4 \/ ~p__1 \/ ~p__8
*********** [30,34,36,201->202] ***********
p__2
p__3
~sk0=sk1 \/ ~sk2=sk3 \/ ~p__2 \/ ~p__3
sk0=sk4 \/ ~p__1 \/ ~p__8
-----------------------------
~sk1=sk4 \/ ~sk2=sk3 \/ ~p__1 \/ ~p__8
*********** [30,34,72,102->203] ***********
p__2
p__3
f(g(sk1))=sk1 \/ g(f(sk3))=sk3 \/ ~p__2 \/ ~p__3
~f(g(X0))=X0 \/ sk4=X0 \/ ~p__1
-----------------------------
g(f(sk3))=sk3 \/ sk1=sk4 \/ ~p__1
*********** [97,106,203->204] ***********
~p__0
~g(f(X0))=X0 \/ ~g(f(X1))=X1 \/ X0=X1 \/ p__0
g(f(sk3))=sk3 \/ sk1=sk4 \/ ~p__1
-----------------------------
sk1=sk4 \/ ~p__1 \/ ~p__8
*********** [202,204->205] ***********
~sk1=sk4 \/ ~sk2=sk3 \/ ~p__1 \/ ~p__8
sk1=sk4 \/ ~p__1 \/ ~p__8
-----------------------------
~sk2=sk3 \/ ~p__1 \/ ~p__8
*********** [30,34,72,131->206] ***********
p__2
p__3
f(g(sk1))=sk1 \/ g(f(sk3))=sk3 \/ ~p__2 \/ ~p__3
~g(f(X0))=X0 \/ g(sk0)=X0 \/ p__4
-----------------------------
g(f(sk3))=sk3 \/ g(sk0)=g(sk1) \/ p__4
*********** [97,185,106,206->207] ***********
~p__0
~p__4
~g(f(X0))=X0 \/ ~g(f(X1))=X1 \/ X0=X1 \/ p__0
g(f(sk3))=sk3 \/ g(sk0)=g(sk1) \/ p__4
-----------------------------
g(sk0)=g(sk1) \/ ~p__8
*********** [30,34,86,201->208] ***********
p__2
p__3
~sk0=sk1 \/ g(f(sk3))=sk3 \/ ~p__2 \/ ~p__3
sk0=sk4 \/ ~p__1 \/ ~p__8
-----------------------------
~sk1=sk4 \/ g(f(sk3))=sk3 \/ ~p__1 \/ ~p__8
*********** [208,204->209] ***********
~sk1=sk4 \/ g(f(sk3))=sk3 \/ ~p__1 \/ ~p__8
sk1=sk4 \/ ~p__1 \/ ~p__8
-----------------------------
g(f(sk3))=sk3 \/ ~p__1 \/ ~p__8
*********** [204,207,185,131,209->210] ***********
sk1=sk4 \/ ~p__1 \/ ~p__8
g(sk0)=g(sk1) \/ ~p__8
~p__4
~g(f(X0))=X0 \/ g(sk0)=X0 \/ p__4
g(f(sk3))=sk3 \/ ~p__1 \/ ~p__8
-----------------------------
g(sk4)=sk3 \/ ~p__1 \/ ~p__8
*********** [30,34,92,201->211] ***********
p__2
p__3
~sk0=sk1 \/ g(f(sk2))=sk2 \/ ~p__2 \/ ~p__3
sk0=sk4 \/ ~p__1 \/ ~p__8
-----------------------------
~sk1=sk4 \/ g(f(sk2))=sk2 \/ ~p__1 \/ ~p__8
*********** [211,204->212] ***********
~sk1=sk4 \/ g(f(sk2))=sk2 \/ ~p__1 \/ ~p__8
sk1=sk4 \/ ~p__1 \/ ~p__8
-----------------------------
g(f(sk2))=sk2 \/ ~p__1 \/ ~p__8
*********** [210,204,207,185,131,212->213] ***********
g(sk4)=sk3 \/ ~p__1 \/ ~p__8
sk1=sk4 \/ ~p__1 \/ ~p__8
g(sk0)=g(sk1) \/ ~p__8
~p__4
~g(f(X0))=X0 \/ g(sk0)=X0 \/ p__4
g(f(sk2))=sk2 \/ ~p__1 \/ ~p__8
-----------------------------
sk2=sk3 \/ ~p__1 \/ ~p__8
*********** [205,213->214] ***********
~sk2=sk3 \/ ~p__1 \/ ~p__8
sk2=sk3 \/ ~p__1 \/ ~p__8
-----------------------------
~p__8 \/ ~p__1
*********** [99,32->215] ***********
g(f(sk5))=sk5 \/ p__1
~f(g(X0))=X0 \/ p__3
-----------------------------
p__3 \/ p__1
*********** [30,215,72,118->216] ***********
p__2
p__3 \/ p__1
f(g(sk1))=sk1 \/ g(f(sk3))=sk3 \/ ~p__2 \/ ~p__3
~g(f(X0))=X0 \/ sk5=X0 \/ p__0 \/ p__1
-----------------------------
g(f(sk3))=sk3 \/ g(sk1)=sk5 \/ p__0 \/ p__1
*********** [97,106,216->217] ***********
~p__0
~g(f(X0))=X0 \/ ~g(f(X1))=X1 \/ X0=X1 \/ p__0
g(f(sk3))=sk3 \/ g(sk1)=sk5 \/ p__0 \/ p__1
-----------------------------
~g(f(X0))=X0 \/ sk3=X0 \/ p__8
*********** [166,30,34,92,199->218] ***********
sk1=sk4 \/ ~p__1
p__2
p__3
~sk0=sk1 \/ g(f(sk2))=sk2 \/ ~p__2 \/ ~p__3
sk0=sk4 \/ ~p__1
-----------------------------
g(f(sk2))=sk2 \/ ~p__1
*********** [214,217,218->219] ***********
~p__8 \/ ~p__1
~g(f(X0))=X0 \/ sk3=X0 \/ p__8
g(f(sk2))=sk2 \/ ~p__1
-----------------------------
sk2=sk3 \/ ~p__1
*********** [200,219->220] ***********
~sk2=sk3 \/ ~p__1
sk2=sk3 \/ ~p__1
-----------------------------
~p__1
*********** [30,215,67,118->221] ***********
p__2
p__3 \/ p__1
f(g(sk1))=sk1 \/ g(f(sk2))=sk2 \/ ~p__2 \/ ~p__3
~g(f(X0))=X0 \/ sk5=X0 \/ p__0 \/ p__1
-----------------------------
g(f(sk2))=sk2 \/ g(sk1)=sk5 \/ p__0 \/ p__1
*********** [97,106,221->222] ***********
~p__0
~g(f(X0))=X0 \/ ~g(f(X1))=X1 \/ X0=X1 \/ p__0
g(f(sk2))=sk2 \/ g(sk1)=sk5 \/ p__0 \/ p__1
-----------------------------
~g(f(X0))=X0 \/ sk2=X0 \/ p__9
*********** [99,222->223] ***********
g(f(sk5))=sk5 \/ p__1
~g(f(X0))=X0 \/ sk2=X0 \/ p__9
-----------------------------
sk2=sk5 \/ p__1 \/ p__9
*********** [30,34,43,146->224] ***********
p__2
p__3
f(g(sk0))=sk0 \/ g(f(sk2))=sk2 \/ ~p__2 \/ ~p__3
g(sk0)=sk5 \/ p__1 \/ p__4
-----------------------------
g(f(sk2))=sk2 \/ f(sk5)=sk0 \/ p__1 \/ p__4
*********** [97,185,106,224->225] ***********
~p__0
~p__4
~g(f(X0))=X0 \/ ~g(f(X1))=X1 \/ X0=X1 \/ p__0
g(f(sk2))=sk2 \/ f(sk5)=sk0 \/ p__1 \/ p__4
-----------------------------
f(sk5)=sk0 \/ p__1 \/ ~p__9
*********** [30,34,67,151->226] ***********
p__2
p__3
f(g(sk1))=sk1 \/ g(f(sk2))=sk2 \/ ~p__2 \/ ~p__3
g(sk1)=sk5 \/ p__1
-----------------------------
g(f(sk2))=sk2 \/ f(sk5)=sk1 \/ p__1
*********** [97,220,106,226->227] ***********
~p__0
~p__1
~g(f(X0))=X0 \/ ~g(f(X1))=X1 \/ X0=X1 \/ p__0
g(f(sk2))=sk2 \/ f(sk5)=sk1 \/ p__1
-----------------------------
f(sk5)=sk1 \/ ~p__9
*********** [220,225,227->228] ***********
~p__1
f(sk5)=sk0 \/ p__1 \/ ~p__9
f(sk5)=sk1 \/ ~p__9
-----------------------------
sk0=sk1 \/ ~p__9
*********** [30,34,92,228->229] ***********
p__2
p__3
~sk0=sk1 \/ g(f(sk2))=sk2 \/ ~p__2 \/ ~p__3
sk0=sk1 \/ ~p__9
-----------------------------
g(f(sk2))=sk2 \/ ~p__9
*********** [97,220,223,118,229->230] ***********
~p__0
~p__1
sk2=sk5 \/ p__1 \/ p__9
~g(f(X0))=X0 \/ sk5=X0 \/ p__0 \/ p__1
g(f(sk2))=sk2 \/ ~p__9
-----------------------------
sk2=sk5
*********** [30,34,36,230->231] ***********
p__2
p__3
~sk0=sk1 \/ ~sk2=sk3 \/ ~p__2 \/ ~p__3
sk2=sk5
-----------------------------
~sk0=sk1 \/ ~sk3=sk5
*********** [97,217,106,209->232] ***********
~p__0
~g(f(X0))=X0 \/ sk3=X0 \/ p__8
~g(f(X0))=X0 \/ ~g(f(X1))=X1 \/ X0=X1 \/ p__0
g(f(sk3))=sk3 \/ ~p__1 \/ ~p__8
-----------------------------
~g(f(X0))=X0 \/ sk3=X0 \/ ~p__1
*********** [30,34,49,147->233] ***********
p__2
p__3
f(g(sk0))=sk0 \/ g(f(sk3))=sk3 \/ ~p__2 \/ ~p__3
g(sk0)=sk5 \/ p__0 \/ p__1
-----------------------------
g(f(sk3))=sk3 \/ f(sk5)=sk0 \/ p__0 \/ p__1
*********** [97,232,106,233->234] ***********
~p__0
~g(f(X0))=X0 \/ sk3=X0 \/ ~p__1
~g(f(X0))=X0 \/ ~g(f(X1))=X1 \/ X0=X1 \/ p__0
g(f(sk3))=sk3 \/ f(sk5)=sk0 \/ p__0 \/ p__1
-----------------------------
f(sk5)=sk0 \/ ~p__8
*********** [30,34,72,151->235] ***********
p__2
p__3
f(g(sk1))=sk1 \/ g(f(sk3))=sk3 \/ ~p__2 \/ ~p__3
g(sk1)=sk5 \/ p__1
-----------------------------
g(f(sk3))=sk3 \/ f(sk5)=sk1 \/ p__1
*********** [97,220,106,235->236] ***********
~p__0
~p__1
~g(f(X0))=X0 \/ ~g(f(X1))=X1 \/ X0=X1 \/ p__0
g(f(sk3))=sk3 \/ f(sk5)=sk1 \/ p__1
-----------------------------
f(sk5)=sk1 \/ ~p__8
*********** [234,236->237] ***********
f(sk5)=sk0 \/ ~p__8
f(sk5)=sk1 \/ ~p__8
-----------------------------
sk0=sk1 \/ ~p__8
*********** [237,231->238] ***********
sk0=sk1 \/ ~p__8
~sk0=sk1 \/ ~sk3=sk5
-----------------------------
~sk3=sk5 \/ ~p__8
*********** [207,97,106,234->239] ***********
g(sk0)=g(sk1) \/ ~p__8
~p__0
~g(f(X0))=X0 \/ ~g(f(X1))=X1 \/ X0=X1 \/ p__0
f(sk5)=sk0 \/ ~p__8
-----------------------------
~g(sk1)=sk5 \/ ~p__8 \/ ~p__12
*********** [207,214,99,234->240] ***********
g(sk0)=g(sk1) \/ ~p__8
~p__8 \/ ~p__1
g(f(sk5))=sk5 \/ p__1
f(sk5)=sk0 \/ ~p__8
-----------------------------
g(sk1)=sk5 \/ ~p__8
*********** [239,240->241] ***********
~g(sk1)=sk5 \/ ~p__8 \/ ~p__12
g(sk1)=sk5 \/ ~p__8
-----------------------------
~p__12 \/ ~p__8
*********** [28,131->242] ***********
f(g(sk4))=sk4 \/ g(f(sk5))=sk5
~g(f(X0))=X0 \/ g(sk0)=X0 \/ p__4
-----------------------------
g(f(sk5))=sk5 \/ g(sk0)=g(sk4) \/ p__4
*********** [97,185,106,242->243] ***********
~p__0
~p__4
~g(f(X0))=X0 \/ ~g(f(X1))=X1 \/ X0=X1 \/ p__0
g(f(sk5))=sk5 \/ g(sk0)=g(sk4) \/ p__4
-----------------------------
~g(f(X0))=X0 \/ sk5=X0 \/ p__12
*********** [30,34,86,237->244] ***********
p__2
p__3
~sk0=sk1 \/ g(f(sk3))=sk3 \/ ~p__2 \/ ~p__3
sk0=sk1 \/ ~p__8
-----------------------------
g(f(sk3))=sk3 \/ ~p__8
*********** [241,243,244->245] ***********
~p__12 \/ ~p__8
~g(f(X0))=X0 \/ sk5=X0 \/ p__12
g(f(sk3))=sk3 \/ ~p__8
-----------------------------
sk3=sk5 \/ ~p__8
*********** [238,245->246] ***********
~sk3=sk5 \/ ~p__8
sk3=sk5 \/ ~p__8
-----------------------------
~p__8
*********** [97,220,118,235->247] ***********
~p__0
~p__1
~g(f(X0))=X0 \/ sk5=X0 \/ p__0 \/ p__1
g(f(sk3))=sk3 \/ f(sk5)=sk1 \/ p__1
-----------------------------
f(sk5)=sk1 \/ sk3=sk5
*********** [246,217,247->248] ***********
~p__8
~g(f(X0))=X0 \/ sk3=X0 \/ p__8
f(sk5)=sk1 \/ sk3=sk5
-----------------------------
~g(sk1)=sk5 \/ sk3=sk5
*********** [220,151,248->249] ***********
~p__1
g(sk1)=sk5 \/ p__1
~g(sk1)=sk5 \/ sk3=sk5
-----------------------------
sk3=sk5
*********** [231,249->250] ***********
~sk0=sk1 \/ ~sk3=sk5
sk3=sk5
-----------------------------
~sk0=sk1
*********** [30,34,36,228->251] ***********
p__2
p__3
~sk0=sk1 \/ ~sk2=sk3 \/ ~p__2 \/ ~p__3
sk0=sk1 \/ ~p__9
-----------------------------
~sk2=sk3 \/ ~p__9
*********** [251,230->252] ***********
~sk2=sk3 \/ ~p__9
sk2=sk5
-----------------------------
~sk3=sk5 \/ ~p__9
*********** [97,113,106,142->253] ***********
~p__0
~g(f(X0))=X0 \/ g(sk1)=X0 \/ p__6
~g(f(X0))=X0 \/ ~g(f(X1))=X1 \/ X0=X1 \/ p__0
f(g(sk1))=sk1 \/ ~p__6
-----------------------------
~g(f(X0))=X0 \/ g(sk1)=X0
*********** [253,229->254] ***********
~g(f(X0))=X0 \/ g(sk1)=X0
g(f(sk2))=sk2 \/ ~p__9
-----------------------------
g(sk1)=sk2 \/ ~p__9
*********** [254,230->255] ***********
g(sk1)=sk2 \/ ~p__9
sk2=sk5
-----------------------------
g(sk1)=sk5 \/ ~p__9
*********** [30,34,86,228->256] ***********
p__2
p__3
~sk0=sk1 \/ g(f(sk3))=sk3 \/ ~p__2 \/ ~p__3
sk0=sk1 \/ ~p__9
-----------------------------
g(f(sk3))=sk3 \/ ~p__9
*********** [255,253,256->257] ***********
g(sk1)=sk5 \/ ~p__9
~g(f(X0))=X0 \/ g(sk1)=X0
g(f(sk3))=sk3 \/ ~p__9
-----------------------------
sk3=sk5 \/ ~p__9
*********** [252,257->258] ***********
~sk3=sk5 \/ ~p__9
sk3=sk5 \/ ~p__9
-----------------------------
~p__9
*********** [151,30,34,59,223->259] ***********
g(sk1)=sk5 \/ p__1
p__2
p__3
~sk2=sk3 \/ f(g(sk1))=sk1 \/ ~p__2 \/ ~p__3
sk2=sk5 \/ p__1 \/ p__9
-----------------------------
~sk3=sk5 \/ f(sk5)=sk1 \/ p__1 \/ p__9
*********** [220,258,259,249->260] ***********
~p__1
~p__9
~sk3=sk5 \/ f(sk5)=sk1 \/ p__1 \/ p__9
sk3=sk5
-----------------------------
f(sk5)=sk1
*********** [30,34,54,230->261] ***********
p__2
p__3
~sk2=sk3 \/ f(g(sk0))=sk0 \/ ~p__2 \/ ~p__3
sk2=sk5
-----------------------------
~sk3=sk5 \/ f(g(sk0))=sk0
*********** [261,249->262] ***********
~sk3=sk5 \/ f(g(sk0))=sk0
sk3=sk5
-----------------------------
f(g(sk0))=sk0
*********** [30,34,67,131->263] ***********
p__2
p__3
f(g(sk1))=sk1 \/ g(f(sk2))=sk2 \/ ~p__2 \/ ~p__3
~g(f(X0))=X0 \/ g(sk0)=X0 \/ p__4
-----------------------------
g(f(sk2))=sk2 \/ g(sk0)=g(sk1) \/ p__4
*********** [185,131,263->264] ***********
~p__4
~g(f(X0))=X0 \/ g(sk0)=X0 \/ p__4
g(f(sk2))=sk2 \/ g(sk0)=g(sk1) \/ p__4
-----------------------------
g(sk0)=g(sk1) \/ g(sk0)=sk2
*********** [264,230->265] ***********
g(sk0)=g(sk1) \/ g(sk0)=sk2
sk2=sk5
-----------------------------
g(sk0)=g(sk1) \/ g(sk0)=sk5
*********** [30,34,67,222->266] ***********
p__2
p__3
f(g(sk1))=sk1 \/ g(f(sk2))=sk2 \/ ~p__2 \/ ~p__3
~g(f(X0))=X0 \/ sk2=X0 \/ p__9
-----------------------------
g(f(sk2))=sk2 \/ g(sk1)=sk2 \/ p__9
*********** [255,266,230->267] ***********
g(sk1)=sk5 \/ ~p__9
g(f(sk2))=sk2 \/ g(sk1)=sk2 \/ p__9
sk2=sk5
-----------------------------
g(f(sk5))=sk5 \/ g(sk1)=sk5
*********** [267,260->268] ***********
g(f(sk5))=sk5 \/ g(sk1)=sk5
f(sk5)=sk1
-----------------------------
g(sk1)=sk5
*********** [265,268->269] ***********
g(sk0)=g(sk1) \/ g(sk0)=sk5
g(sk1)=sk5
-----------------------------
g(sk0)=sk5
*********** [260,262,269->270] ***********
f(sk5)=sk1
f(g(sk0))=sk0
g(sk0)=sk5
-----------------------------
sk0=sk1
*********** [250,270->271] ***********
~sk0=sk1
sk0=sk1
-----------------------------
#
======= End of refutation =======```

### Sample solution for COL003-20

```Refutation found. Thanks to Tanya!
=========== Refutation ==========
*********** [9] ***********
~apply(strong_fixed_point,fixed_pt)=apply(fixed_pt,apply(strong_fixed_point,fixed_pt))
*********** [9->10] ***********
~apply(strong_fixed_point,fixed_pt)=apply(fixed_pt,apply(strong_fixed_point,fixed_pt))
-----------------------------
~p__0(apply(strong_fixed_point,fixed_pt))
*********** [10->11] ***********
~p__0(apply(strong_fixed_point,fixed_pt))
-----------------------------
~p__0(apply(strong_fixed_point,fixed_pt))
*********** [9->12] ***********
~apply(strong_fixed_point,fixed_pt)=apply(fixed_pt,apply(strong_fixed_point,fixed_pt))
-----------------------------
p__0(apply(fixed_pt,apply(strong_fixed_point,fixed_pt)))
*********** [12->13] ***********
p__0(apply(fixed_pt,apply(strong_fixed_point,fixed_pt)))
-----------------------------
p__0(apply(fixed_pt,apply(strong_fixed_point,fixed_pt)))
*********** [4] ***********
apply(apply(apply(b,X0),X1),X2)=apply(X0,apply(X1,X2))
*********** [4->14] ***********
apply(apply(apply(b,X0),X1),X2)=apply(X0,apply(X1,X2))
-----------------------------
apply(apply(apply(b,X0),X1),X2)=apply(X0,apply(X1,X2))
*********** [14->15] ***********
apply(apply(apply(b,X0),X1),X2)=apply(X0,apply(X1,X2))
-----------------------------
apply(apply(apply(b,X0),X1),X2)=apply(X0,apply(X1,X2))
*********** [5] ***********
apply(apply(w,X0),X1)=apply(apply(X0,X1),X1)
*********** [5->16] ***********
apply(apply(w,X0),X1)=apply(apply(X0,X1),X1)
-----------------------------
apply(apply(w,X0),X1)=apply(apply(X0,X1),X1)
*********** [16->17] ***********
apply(apply(w,X0),X1)=apply(apply(X0,X1),X1)
-----------------------------
apply(apply(w,X0),X1)=apply(apply(X0,X1),X1)
*********** [8] ***********
strong_fixed_point=apply(apply(b,apply(w,w)),apply(apply(b,apply(b,w)),apply(apply(b,b),b)))
*********** [8->18] ***********
strong_fixed_point=apply(apply(b,apply(w,w)),apply(apply(b,apply(b,w)),apply(apply(b,b),b)))
-----------------------------
apply(apply(b,apply(w,w)),apply(apply(b,apply(b,w)),apply(apply(b,b),b)))=strong_fixed_point
*********** [17,17,18->19] ***********
apply(apply(w,X0),X1)=apply(apply(X0,X1),X1)
apply(apply(w,X0),X1)=apply(apply(X0,X1),X1)
apply(apply(b,apply(w,w)),apply(apply(b,apply(b,w)),apply(apply(b,b),b)))=strong_fixed_point
-----------------------------
apply(apply(b,apply(w,w)),apply(apply(b,apply(b,w)),apply(apply(w,w),b)))=strong_fixed_point
*********** [15,15,19->20] ***********
apply(apply(apply(b,X0),X1),X2)=apply(X0,apply(X1,X2))
apply(apply(apply(b,X0),X1),X2)=apply(X0,apply(X1,X2))
apply(apply(b,apply(w,w)),apply(apply(b,apply(b,w)),apply(apply(w,w),b)))=strong_fixed_point
-----------------------------
apply(apply(w,w),apply(apply(b,w),apply(apply(apply(w,w),b),X0)))=apply(strong_fixed_point,X0)
*********** [17,17->21] ***********
apply(apply(w,X0),X1)=apply(apply(X0,X1),X1)
apply(apply(w,X0),X1)=apply(apply(X0,X1),X1)
-----------------------------
apply(apply(w,w),X0)=apply(apply(X0,X0),X0)
*********** [15,21->22] ***********
apply(apply(apply(b,X0),X1),X2)=apply(X0,apply(X1,X2))
apply(apply(w,w),X0)=apply(apply(X0,X0),X0)
-----------------------------
apply(apply(apply(w,w),b),X0)=apply(b,apply(b,X0))
*********** [20,22->23] ***********
apply(apply(w,w),apply(apply(b,w),apply(apply(apply(w,w),b),X0)))=apply(strong_fixed_point,X0)
apply(apply(apply(w,w),b),X0)=apply(b,apply(b,X0))
-----------------------------
apply(apply(w,w),apply(apply(b,w),apply(b,apply(b,X0))))=apply(strong_fixed_point,X0)
*********** [15,17->24] ***********
apply(apply(apply(b,X0),X1),X2)=apply(X0,apply(X1,X2))
apply(apply(w,X0),X1)=apply(apply(X0,X1),X1)
-----------------------------
apply(apply(w,apply(b,X0)),X1)=apply(X0,apply(X1,X1))
*********** [15,24->25] ***********
apply(apply(apply(b,X0),X1),X2)=apply(X0,apply(X1,X2))
apply(apply(w,apply(b,X0)),X1)=apply(X0,apply(X1,X1))
-----------------------------
apply(apply(apply(w,apply(b,apply(b,X0))),X1),X2)=apply(X0,apply(apply(X1,X1),X2))
*********** [17,21,25->26] ***********
apply(apply(w,X0),X1)=apply(apply(X0,X1),X1)
apply(apply(w,w),X0)=apply(apply(X0,X0),X0)
apply(apply(apply(w,apply(b,apply(b,X0))),X1),X2)=apply(X0,apply(apply(X1,X1),X2))
-----------------------------
apply(apply(w,apply(w,apply(b,apply(b,X0)))),X1)=apply(X0,apply(apply(w,w),X1))
*********** [15,17->27] ***********
apply(apply(apply(b,X0),X1),X2)=apply(X0,apply(X1,X2))
apply(apply(w,X0),X1)=apply(apply(X0,X1),X1)
-----------------------------
apply(apply(w,apply(apply(b,X0),X1)),X2)=apply(apply(X0,apply(X1,X2)),X2)
*********** [17,17,17->28] ***********
apply(apply(w,X0),X1)=apply(apply(X0,X1),X1)
apply(apply(w,X0),X1)=apply(apply(X0,X1),X1)
apply(apply(w,X0),X1)=apply(apply(X0,X1),X1)
-----------------------------
apply(apply(w,apply(w,X0)),X1)=apply(apply(w,apply(X0,X1)),X1)
*********** [27,28->29] ***********
apply(apply(w,apply(apply(b,X0),X1)),X2)=apply(apply(X0,apply(X1,X2)),X2)
apply(apply(w,apply(w,X0)),X1)=apply(apply(w,apply(X0,X1)),X1)
-----------------------------
apply(apply(w,apply(apply(b,w),X0)),X1)=apply(apply(w,apply(w,X0)),X1)
*********** [17,29->30] ***********
apply(apply(w,X0),X1)=apply(apply(X0,X1),X1)
apply(apply(w,apply(apply(b,w),X0)),X1)=apply(apply(w,apply(w,X0)),X1)
-----------------------------
apply(apply(w,apply(w,X0)),apply(apply(b,w),X0))=apply(apply(w,w),apply(apply(b,w),X0))
*********** [23,23,26,30->31] ***********
apply(apply(w,w),apply(apply(b,w),apply(b,apply(b,X0))))=apply(strong_fixed_point,X0)
apply(apply(w,w),apply(apply(b,w),apply(b,apply(b,X0))))=apply(strong_fixed_point,X0)
apply(apply(w,apply(w,apply(b,apply(b,X0)))),X1)=apply(X0,apply(apply(w,w),X1))
apply(apply(w,apply(w,X0)),apply(apply(b,w),X0))=apply(apply(w,w),apply(apply(b,w),X0))
-----------------------------
apply(X0,apply(strong_fixed_point,X0))=apply(strong_fixed_point,X0)
*********** [11,13,31->32] ***********
~p__0(apply(strong_fixed_point,fixed_pt))
p__0(apply(fixed_pt,apply(strong_fixed_point,fixed_pt)))
apply(X0,apply(strong_fixed_point,X0))=apply(strong_fixed_point,X0)
-----------------------------
#
======= End of refutation ======= ```