WATCH: 0.00 CPU 0.01 WC
% Vampire version 0.6 licenced to run at CASC-J5
% Any licence to use Vampire shall only be obtained
% as described on Vampire's home page http://www.vprover.org.
Hi Geoff, go and have some cold beer while I am trying to solve this very hard problem!
% remaining time: 2999 next slice time: 67
lrs+1004_20_bs=off:drc=off:flr=on:fsr=off:fde=none:gsp=input_only:lcm=reverse:nwc=1.7:ssec=off:stl=60:sac=on:sgo=on:sio=off:spo=on:updr=off_49 on FEQ061

WATCH: 2.98 CPU 3.03 WC

WATCH: 5.98 CPU 6.04 WC
Time limit reached!
------------------------------
Version: Vampire 1.0 (revision 700)
Termination reason: Time limit
Termination phase: Saturation

Active clauses: 2635
Passive clauses: 23750
Generated clauses: 597488
Input formulas: 27
Initial clauses: 30

Splitted inequalities: 1

Trivial inequalities: 86
Fw demodulations: 293692
Bw demodulations: 9834
Fw literal rewrites: 226

Simple tautologies: 226
Forward subsumptions: 276632
Fw demodulations to eq. taut.: 2826
Bw demodulations to eq. taut.: 828

Binary resolution: 92
Forward superposition: 148150
Backward superposition: 145131
Self superposition: 247

Unique components: 2454

Memory used: 238716KB
Time elapsed: 6.800 s
------------------------------
% remaining time: 2931 next slice time: 775
lrs-1004_20_bs=off:bms=on:cond=fast:drc=off:flr=on:nwc=1.1:stl=60:sio=off:spl=off:sfv=off:updr=off_574 on FEQ061

WATCH: 8.98 CPU 9.06 WC

WATCH: 12.00 CPU 12.07 WC

WATCH: 15.01 CPU 15.08 WC

WATCH: 18.02 CPU 18.09 WC

WATCH: 21.03 CPU 21.10 WC

WATCH: 24.04 CPU 24.11 WC

WATCH: 27.06 CPU 27.12 WC

WATCH: 30.06 CPU 30.13 WC

WATCH: 33.06 CPU 33.14 WC

WATCH: 36.09 CPU 36.15 WC

WATCH: 39.09 CPU 39.16 WC
Refutation found. Thanks to Tanya!
% SZS status Theorem for FEQ061
% SZS output start Proof for FEQ061
fof(f1752201,plain,(
  $false),
  inference(subsumption_resolution,[],[f1752200,f70])).
fof(f70,plain,(
  sP0(one)),
  inference(inequality_splitting,[],[f67,f69])).
fof(f69,plain,(
  ~sP0(addition(antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sK1))))))))))))),antidomain(antidomain(sK2))))),
  introduced(inequality_splitting_name_introduction,[])).
fof(f67,plain,(
  addition(antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sK1))))))))))))),antidomain(antidomain(sK2))) != one),
  inference(definition_unfolding,[],[f33,f63,f42,f42])).
fof(f42,plain,(
  ( ! [X0] : (antidomain(antidomain(X0)) = domain(X0)) )),
  inference(cnf_transformation,[],[f16])).
fof(f16,axiom,(
  ! [X0] : antidomain(antidomain(X0)) = domain(X0)),
  file('/CW/home-0/sutcliff/CASC/23/Problems/FEQ/FEQ061.p',domain4)).
fof(f63,plain,(
  ( ! [X0,X1] : (antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(X0,antidomain(antidomain(antidomain(antidomain(antidomain(X1))))))))))) = forward_box(X0,X1)) )),
  inference(definition_unfolding,[],[f48,f61,f62,f61])).
fof(f62,plain,(
  ( ! [X0,X1] : (antidomain(antidomain(multiplication(X0,antidomain(antidomain(X1))))) = forward_diamond(X0,X1)) )),
  inference(definition_unfolding,[],[f51,f42,f42])).
fof(f51,plain,(
  ( ! [X0,X1] : (domain(multiplication(X0,domain(X1))) = forward_diamond(X0,X1)) )),
  inference(cnf_transformation,[],[f23])).
fof(f23,axiom,(
  ! [X0,X1] : domain(multiplication(X0,domain(X1))) = forward_diamond(X0,X1)),
  file('/CW/home-0/sutcliff/CASC/23/Problems/FEQ/FEQ061.p',forward_diamond)).
fof(f61,plain,(
  ( ! [X0] : (antidomain(antidomain(antidomain(X0))) = c(X0)) )),
  inference(definition_unfolding,[],[f43,f42])).
fof(f43,plain,(
  ( ! [X0] : (antidomain(domain(X0)) = c(X0)) )),
  inference(cnf_transformation,[],[f22])).
fof(f22,axiom,(
  ! [X0] : antidomain(domain(X0)) = c(X0)),
  file('/CW/home-0/sutcliff/CASC/23/Problems/FEQ/FEQ061.p',complement)).
fof(f48,plain,(
  ( ! [X0,X1] : (c(forward_diamond(X0,c(X1))) = forward_box(X0,X1)) )),
  inference(cnf_transformation,[],[f26])).
fof(f26,axiom,(
  ! [X0,X1] : c(forward_diamond(X0,c(X1))) = forward_box(X0,X1)),
  file('/CW/home-0/sutcliff/CASC/23/Problems/FEQ/FEQ061.p',forward_box)).
fof(f33,plain,(
  addition(forward_box(sK0,domain(sK1)),domain(sK2)) != one),
  inference(cnf_transformation,[],[f30])).
fof(f30,plain,(
  addition(domain(sK1),backward_box(sK0,domain(sK2))) = one & addition(forward_box(sK0,domain(sK1)),domain(sK2)) != one),
  inference(skolemisation,[status(esa)],[f29])).
fof(f29,plain,(
  ? [X0,X1,X2] : (addition(domain(X1),backward_box(X0,domain(X2))) = one & addition(forward_box(X0,domain(X1)),domain(X2)) != one)),
  inference(ennf_transformation,[],[f27])).
fof(f27,negated_conjecture,(
  ~! [X0,X1,X2] : (addition(domain(X1),backward_box(X0,domain(X2))) = one => addition(forward_box(X0,domain(X1)),domain(X2)) = one)),
  file('/CW/home-0/sutcliff/CASC/23/Problems/FEQ/FEQ061.p',goals)).
fof(f1752200,plain,(
  ~sP0(one)),
  inference(backward_demodulation,[],[f1752195,f4846])).
fof(f4846,plain,(
  ~sP0(addition(antidomain(antidomain(sK2)),antidomain(multiplication(sK0,antidomain(sK1)))))),
  inference(forward_demodulation,[],[f4845,f4813])).
fof(f4813,plain,(
  ( ! [X60] : (antidomain(X60) = antidomain(antidomain(antidomain(X60)))) )),
  inference(forward_demodulation,[],[f4812,f3719])).
fof(f3719,plain,(
  ( ! [X0] : (multiplication(antidomain(antidomain(X0)),X0) = X0) )),
  inference(forward_demodulation,[],[f3674,f37])).
fof(f37,plain,(
  ( ! [X0] : (multiplication(one,X0) = X0) )),
  inference(cnf_transformation,[],[f8])).
fof(f8,axiom,(
  ! [X0] : multiplication(one,X0) = X0),
  file('/CW/home-0/sutcliff/CASC/23/Problems/FEQ/FEQ061.p',multiplicative_left_identity)).
fof(f3674,plain,(
  ( ! [X0] : (multiplication(one,X0) = multiplication(antidomain(antidomain(X0)),X0)) )),
  inference(superposition,[],[f3545,f71])).
fof(f71,plain,(
  ( ! [X0] : (addition(antidomain(X0),antidomain(antidomain(X0))) = one) )),
  inference(backward_demodulation,[],[f47,f45])).
fof(f45,plain,(
  ( ! [X0] : (addition(antidomain(antidomain(X0)),antidomain(X0)) = one) )),
  inference(cnf_transformation,[],[f13])).
fof(f13,axiom,(
  ! [X0] : addition(antidomain(antidomain(X0)),antidomain(X0)) = one),
  file('/CW/home-0/sutcliff/CASC/23/Problems/FEQ/FEQ061.p',domain3)).
fof(f47,plain,(
  ( ! [X0,X1] : (addition(X0,X1) = addition(X1,X0)) )),
  inference(cnf_transformation,[],[f12])).
fof(f12,axiom,(
  ! [X0,X1] : addition(X0,X1) = addition(X1,X0)),
  file('/CW/home-0/sutcliff/CASC/23/Problems/FEQ/FEQ061.p',additive_commutativity)).
fof(f3545,plain,(
  ( ! [X41,X40] : (multiplication(X41,X40) = multiplication(addition(antidomain(X40),X41),X40)) )),
  inference(forward_demodulation,[],[f3457,f80])).
fof(f80,plain,(
  ( ! [X0] : (addition(zero,X0) = X0) )),
  inference(superposition,[],[f47,f34])).
fof(f34,plain,(
  ( ! [X0] : (addition(X0,zero) = X0) )),
  inference(cnf_transformation,[],[f2])).
fof(f2,axiom,(
  ! [X0] : addition(X0,zero) = X0),
  file('/CW/home-0/sutcliff/CASC/23/Problems/FEQ/FEQ061.p',additive_identity)).
fof(f3457,plain,(
  ( ! [X41,X40] : (multiplication(addition(antidomain(X40),X41),X40) = addition(zero,multiplication(X41,X40))) )),
  inference(superposition,[],[f60,f41])).
fof(f41,plain,(
  ( ! [X0] : (multiplication(antidomain(X0),X0) = zero) )),
  inference(cnf_transformation,[],[f19])).
fof(f19,axiom,(
  ! [X0] : multiplication(antidomain(X0),X0) = zero),
  file('/CW/home-0/sutcliff/CASC/23/Problems/FEQ/FEQ061.p',domain1)).
fof(f60,plain,(
  ( ! [X2,X0,X1] : (multiplication(addition(X0,X1),X2) = addition(multiplication(X0,X2),multiplication(X1,X2))) )),
  inference(cnf_transformation,[],[f7])).
fof(f7,axiom,(
  ! [X0,X1,X2] : multiplication(addition(X0,X1),X2) = addition(multiplication(X0,X2),multiplication(X1,X2))),
  file('/CW/home-0/sutcliff/CASC/23/Problems/FEQ/FEQ061.p',left_distributivity)).
fof(f4812,plain,(
  ( ! [X60] : (multiplication(antidomain(antidomain(antidomain(X60))),antidomain(X60)) = antidomain(antidomain(antidomain(X60)))) )),
  inference(forward_demodulation,[],[f4765,f35])).
fof(f35,plain,(
  ( ! [X0] : (multiplication(X0,one) = X0) )),
  inference(cnf_transformation,[],[f11])).
fof(f11,axiom,(
  ! [X0] : multiplication(X0,one) = X0),
  file('/CW/home-0/sutcliff/CASC/23/Problems/FEQ/FEQ061.p',multiplicative_right_identity)).
fof(f4765,plain,(
  ( ! [X60] : (multiplication(antidomain(antidomain(antidomain(X60))),one) = multiplication(antidomain(antidomain(antidomain(X60))),antidomain(X60))) )),
  inference(superposition,[],[f1930,f71])).
fof(f1930,plain,(
  ( ! [X24,X25] : (multiplication(antidomain(X24),X25) = multiplication(antidomain(X24),addition(X25,X24))) )),
  inference(forward_demodulation,[],[f1880,f34])).
fof(f1880,plain,(
  ( ! [X24,X25] : (multiplication(antidomain(X24),addition(X25,X24)) = addition(multiplication(antidomain(X24),X25),zero)) )),
  inference(superposition,[],[f59,f41])).
fof(f59,plain,(
  ( ! [X2,X0,X1] : (multiplication(X0,addition(X1,X2)) = addition(multiplication(X0,X1),multiplication(X0,X2))) )),
  inference(cnf_transformation,[],[f9])).
fof(f9,axiom,(
  ! [X0,X1,X2] : multiplication(X0,addition(X1,X2)) = addition(multiplication(X0,X1),multiplication(X0,X2))),
  file('/CW/home-0/sutcliff/CASC/23/Problems/FEQ/FEQ061.p',right_distributivity)).
fof(f4845,plain,(
  ~sP0(addition(antidomain(antidomain(sK2)),antidomain(multiplication(sK0,antidomain(antidomain(antidomain(sK1)))))))),
  inference(forward_demodulation,[],[f4844,f4813])).
fof(f4844,plain,(
  ~sP0(addition(antidomain(antidomain(sK2)),antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(antidomain(sK1)))))))))),
  inference(forward_demodulation,[],[f4843,f4813])).
fof(f4843,plain,(
  ~sP0(addition(antidomain(antidomain(sK2)),antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sK1)))))))))))),
  inference(forward_demodulation,[],[f4830,f4813])).
fof(f4830,plain,(
  ~sP0(addition(antidomain(antidomain(sK2)),antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sK1)))))))))))))),
  inference(backward_demodulation,[],[f4813,f73])).
fof(f73,plain,(
  ~sP0(addition(antidomain(antidomain(sK2)),antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sK1)))))))))))))))),
  inference(forward_demodulation,[],[f69,f47])).
fof(f1752195,plain,(
  addition(antidomain(antidomain(sK2)),antidomain(multiplication(sK0,antidomain(sK1)))) = one),
  inference(forward_demodulation,[],[f1752194,f4813])).
fof(f1752194,plain,(
  addition(antidomain(antidomain(sK2)),antidomain(antidomain(antidomain(multiplication(sK0,antidomain(sK1)))))) = one),
  inference(forward_demodulation,[],[f1749468,f47])).
fof(f1749468,plain,(
  addition(antidomain(antidomain(antidomain(multiplication(sK0,antidomain(sK1))))),antidomain(antidomain(sK2))) = one),
  inference(superposition,[],[f1745491,f963324])).
fof(f963324,plain,(
  antidomain(antidomain(sK2)) = antidomain(multiplication(antidomain(sK2),antidomain(multiplication(sK0,antidomain(sK1)))))),
  inference(superposition,[],[f963073,f35030])).
fof(f35030,plain,(
  ( ! [X3] : (multiplication(antidomain(sK2),X3) = multiplication(antidomain(sK2),addition(multiplication(sK0,antidomain(sK1)),X3))) )),
  inference(forward_demodulation,[],[f34988,f80])).
fof(f34988,plain,(
  ( ! [X3] : (multiplication(antidomain(sK2),addition(multiplication(sK0,antidomain(sK1)),X3)) = addition(zero,multiplication(antidomain(sK2),X3))) )),
  inference(superposition,[],[f59,f34923])).
fof(f34923,plain,(
  multiplication(antidomain(sK2),multiplication(sK0,antidomain(sK1))) = zero),
  inference(forward_demodulation,[],[f34878,f39])).
fof(f39,plain,(
  ( ! [X0] : (multiplication(X0,zero) = zero) )),
  inference(cnf_transformation,[],[f6])).
fof(f6,axiom,(
  ! [X0] : multiplication(X0,zero) = zero),
  file('/CW/home-0/sutcliff/CASC/23/Problems/FEQ/FEQ061.p',right_annihilation)).
fof(f34878,plain,(
  multiplication(antidomain(sK2),zero) = multiplication(antidomain(sK2),multiplication(sK0,antidomain(sK1)))),
  inference(superposition,[],[f2009,f34831])).
fof(f34831,plain,(
  multiplication(coantidomain(coantidomain(antidomain(sK2))),multiplication(sK0,antidomain(sK1))) = zero),
  inference(forward_demodulation,[],[f34789,f58])).
fof(f58,plain,(
  ( ! [X2,X0,X1] : (multiplication(X0,multiplication(X1,X2)) = multiplication(multiplication(X0,X1),X2)) )),
  inference(cnf_transformation,[],[f1])).
fof(f1,axiom,(
  ! [X0,X1,X2] : multiplication(X0,multiplication(X1,X2)) = multiplication(multiplication(X0,X1),X2)),
  file('/CW/home-0/sutcliff/CASC/23/Problems/FEQ/FEQ061.p',multiplicative_associativity)).
fof(f34789,plain,(
  multiplication(multiplication(coantidomain(coantidomain(antidomain(sK2))),sK0),antidomain(sK1)) = zero),
  inference(superposition,[],[f209,f34695])).
fof(f34695,plain,(
  multiplication(coantidomain(multiplication(coantidomain(coantidomain(antidomain(sK2))),sK0)),antidomain(sK1)) = antidomain(sK1)),
  inference(forward_demodulation,[],[f34630,f37])).
fof(f34630,plain,(
  multiplication(one,antidomain(sK1)) = multiplication(coantidomain(multiplication(coantidomain(coantidomain(antidomain(sK2))),sK0)),antidomain(sK1))),
  inference(superposition,[],[f3545,f34457])).
fof(f34457,plain,(
  addition(antidomain(antidomain(sK1)),coantidomain(multiplication(coantidomain(coantidomain(antidomain(sK2))),sK0))) = one),
  inference(forward_demodulation,[],[f34456,f5161])).
fof(f5161,plain,(
  ( ! [X65] : (coantidomain(X65) = coantidomain(coantidomain(coantidomain(X65)))) )),
  inference(forward_demodulation,[],[f5160,f1983])).
fof(f1983,plain,(
  ( ! [X0] : (multiplication(X0,coantidomain(coantidomain(X0))) = X0) )),
  inference(forward_demodulation,[],[f1952,f35])).
fof(f1952,plain,(
  ( ! [X0] : (multiplication(X0,one) = multiplication(X0,coantidomain(coantidomain(X0)))) )),
  inference(superposition,[],[f1905,f72])).
fof(f72,plain,(
  ( ! [X0] : (addition(coantidomain(X0),coantidomain(coantidomain(X0))) = one) )),
  inference(backward_demodulation,[],[f47,f46])).
fof(f46,plain,(
  ( ! [X0] : (addition(coantidomain(coantidomain(X0)),coantidomain(X0)) = one) )),
  inference(cnf_transformation,[],[f15])).
fof(f15,axiom,(
  ! [X0] : addition(coantidomain(coantidomain(X0)),coantidomain(X0)) = one),
  file('/CW/home-0/sutcliff/CASC/23/Problems/FEQ/FEQ061.p',codomain3)).
fof(f1905,plain,(
  ( ! [X14,X15] : (multiplication(X14,X15) = multiplication(X14,addition(coantidomain(X14),X15))) )),
  inference(forward_demodulation,[],[f1861,f80])).
fof(f1861,plain,(
  ( ! [X14,X15] : (multiplication(X14,addition(coantidomain(X14),X15)) = addition(zero,multiplication(X14,X15))) )),
  inference(superposition,[],[f59,f40])).
fof(f40,plain,(
  ( ! [X0] : (multiplication(X0,coantidomain(X0)) = zero) )),
  inference(cnf_transformation,[],[f20])).
fof(f20,axiom,(
  ! [X0] : multiplication(X0,coantidomain(X0)) = zero),
  file('/CW/home-0/sutcliff/CASC/23/Problems/FEQ/FEQ061.p',codomain1)).
fof(f5160,plain,(
  ( ! [X65] : (multiplication(coantidomain(X65),coantidomain(coantidomain(coantidomain(X65)))) = coantidomain(coantidomain(coantidomain(X65)))) )),
  inference(forward_demodulation,[],[f5124,f37])).
fof(f5124,plain,(
  ( ! [X65] : (multiplication(one,coantidomain(coantidomain(coantidomain(X65)))) = multiplication(coantidomain(X65),coantidomain(coantidomain(coantidomain(X65))))) )),
  inference(superposition,[],[f3507,f72])).
fof(f3507,plain,(
  ( ! [X28,X29] : (multiplication(X29,coantidomain(X28)) = multiplication(addition(X29,X28),coantidomain(X28))) )),
  inference(forward_demodulation,[],[f3420,f34])).
fof(f3420,plain,(
  ( ! [X28,X29] : (multiplication(addition(X29,X28),coantidomain(X28)) = addition(multiplication(X29,coantidomain(X28)),zero)) )),
  inference(superposition,[],[f60,f40])).
fof(f34456,plain,(
  addition(antidomain(antidomain(sK1)),coantidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(sK2))),sK0))))) = one),
  inference(forward_demodulation,[],[f34340,f188])).
fof(f188,plain,(
  ( ! [X13] : (addition(one,coantidomain(X13)) = one) )),
  inference(forward_demodulation,[],[f175,f47])).
fof(f175,plain,(
  ( ! [X13] : (addition(coantidomain(X13),one) = one) )),
  inference(superposition,[],[f143,f72])).
fof(f143,plain,(
  ( ! [X2,X3] : (addition(X2,X3) = addition(X2,addition(X2,X3))) )),
  inference(superposition,[],[f57,f36])).
fof(f36,plain,(
  ( ! [X0] : (addition(X0,X0) = X0) )),
  inference(cnf_transformation,[],[f4])).
fof(f4,axiom,(
  ! [X0] : addition(X0,X0) = X0),
  file('/CW/home-0/sutcliff/CASC/23/Problems/FEQ/FEQ061.p',additive_idempotence)).
fof(f57,plain,(
  ( ! [X2,X0,X1] : (addition(X2,addition(X1,X0)) = addition(addition(X2,X1),X0)) )),
  inference(cnf_transformation,[],[f28])).
fof(f28,plain,(
  ! [X0,X1,X2] : addition(X2,addition(X1,X0)) = addition(addition(X2,X1),X0)),
  inference(rectify,[],[f3])).
fof(f3,axiom,(
  ! [X2,X1,X0] : addition(X0,addition(X1,X2)) = addition(addition(X0,X1),X2)),
  file('/CW/home-0/sutcliff/CASC/23/Problems/FEQ/FEQ061.p',additive_associativity)).
fof(f34340,plain,(
  addition(one,coantidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(sK2))),sK0))))) = addition(antidomain(antidomain(sK1)),coantidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(sK2))),sK0)))))),
  inference(superposition,[],[f5047,f8860])).
fof(f8860,plain,(
  ( ! [X24] : (addition(antidomain(coantidomain(X24)),coantidomain(coantidomain(X24))) = coantidomain(coantidomain(X24))) )),
  inference(forward_demodulation,[],[f8859,f47])).
fof(f8859,plain,(
  ( ! [X24] : (addition(coantidomain(coantidomain(X24)),antidomain(coantidomain(X24))) = coantidomain(coantidomain(X24))) )),
  inference(forward_demodulation,[],[f8858,f37])).
fof(f8858,plain,(
  ( ! [X24] : (multiplication(one,coantidomain(coantidomain(X24))) = addition(coantidomain(coantidomain(X24)),antidomain(coantidomain(X24)))) )),
  inference(forward_demodulation,[],[f8857,f187])).
fof(f187,plain,(
  ( ! [X12] : (addition(one,antidomain(X12)) = one) )),
  inference(forward_demodulation,[],[f174,f47])).
fof(f174,plain,(
  ( ! [X12] : (addition(antidomain(X12),one) = one) )),
  inference(superposition,[],[f143,f71])).
fof(f8857,plain,(
  ( ! [X24] : (multiplication(addition(one,antidomain(coantidomain(X24))),coantidomain(coantidomain(X24))) = addition(coantidomain(coantidomain(X24)),antidomain(coantidomain(X24)))) )),
  inference(forward_demodulation,[],[f8822,f3529])).
fof(f3529,plain,(
  ( ! [X10,X11,X9] : (multiplication(addition(X9,X11),X10) = multiplication(addition(X11,X9),X10)) )),
  inference(forward_demodulation,[],[f3441,f60])).
fof(f3441,plain,(
  ( ! [X10,X11,X9] : (multiplication(addition(X9,X11),X10) = addition(multiplication(X11,X10),multiplication(X9,X10))) )),
  inference(superposition,[],[f60,f47])).
fof(f8822,plain,(
  ( ! [X24] : (multiplication(addition(antidomain(coantidomain(X24)),one),coantidomain(coantidomain(X24))) = addition(coantidomain(coantidomain(X24)),antidomain(coantidomain(X24)))) )),
  inference(superposition,[],[f3510,f2240])).
fof(f2240,plain,(
  ( ! [X62] : (multiplication(antidomain(coantidomain(X62)),coantidomain(coantidomain(X62))) = antidomain(coantidomain(X62))) )),
  inference(forward_demodulation,[],[f2195,f35])).
fof(f2195,plain,(
  ( ! [X62] : (multiplication(antidomain(coantidomain(X62)),one) = multiplication(antidomain(coantidomain(X62)),coantidomain(coantidomain(X62)))) )),
  inference(superposition,[],[f1912,f72])).
fof(f1912,plain,(
  ( ! [X24,X25] : (multiplication(antidomain(X24),X25) = multiplication(antidomain(X24),addition(X24,X25))) )),
  inference(forward_demodulation,[],[f1865,f80])).
fof(f1865,plain,(
  ( ! [X24,X25] : (multiplication(antidomain(X24),addition(X24,X25)) = addition(zero,multiplication(antidomain(X24),X25))) )),
  inference(superposition,[],[f59,f41])).
fof(f3510,plain,(
  ( ! [X39,X38] : (multiplication(addition(X39,one),X38) = addition(X38,multiplication(X39,X38))) )),
  inference(forward_demodulation,[],[f3424,f47])).
fof(f3424,plain,(
  ( ! [X39,X38] : (multiplication(addition(X39,one),X38) = addition(multiplication(X39,X38),X38)) )),
  inference(superposition,[],[f60,f37])).
fof(f5047,plain,(
  ( ! [X0] : (addition(one,X0) = addition(antidomain(antidomain(sK1)),addition(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(sK2))),sK0)))),X0))) )),
  inference(superposition,[],[f57,f4851])).
fof(f4851,plain,(
  addition(antidomain(antidomain(sK1)),antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(sK2))),sK0))))) = one),
  inference(forward_demodulation,[],[f4850,f4813])).
fof(f4850,plain,(
  addition(antidomain(antidomain(sK1)),antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(sK2))))),sK0))))) = one),
  inference(forward_demodulation,[],[f4836,f4813])).
fof(f4836,plain,(
  addition(antidomain(antidomain(sK1)),antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(sK2))))),sK0))))))) = one),
  inference(backward_demodulation,[],[f4813,f68])).
fof(f68,plain,(
  addition(antidomain(antidomain(sK1)),antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sK2))))))),sK0))))))) = one),
  inference(definition_unfolding,[],[f32,f42,f66,f42])).
fof(f66,plain,(
  ( ! [X0,X1] : (antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(X1))))),X0)))))) = backward_box(X0,X1)) )),
  inference(definition_unfolding,[],[f49,f61,f64,f61])).
fof(f64,plain,(
  ( ! [X0,X1] : (coantidomain(coantidomain(multiplication(coantidomain(coantidomain(X1)),X0))) = backward_diamond(X0,X1)) )),
  inference(definition_unfolding,[],[f52,f44,f44])).
fof(f44,plain,(
  ( ! [X0] : (codomain(X0) = coantidomain(coantidomain(X0))) )),
  inference(cnf_transformation,[],[f14])).
fof(f14,axiom,(
  ! [X0] : codomain(X0) = coantidomain(coantidomain(X0))),
  file('/CW/home-0/sutcliff/CASC/23/Problems/FEQ/FEQ061.p',codomain4)).
fof(f52,plain,(
  ( ! [X0,X1] : (codomain(multiplication(codomain(X1),X0)) = backward_diamond(X0,X1)) )),
  inference(cnf_transformation,[],[f21])).
fof(f21,axiom,(
  ! [X0,X1] : codomain(multiplication(codomain(X1),X0)) = backward_diamond(X0,X1)),
  file('/CW/home-0/sutcliff/CASC/23/Problems/FEQ/FEQ061.p',backward_diamond)).
fof(f49,plain,(
  ( ! [X0,X1] : (c(backward_diamond(X0,c(X1))) = backward_box(X0,X1)) )),
  inference(cnf_transformation,[],[f25])).
fof(f25,axiom,(
  ! [X0,X1] : c(backward_diamond(X0,c(X1))) = backward_box(X0,X1)),
  file('/CW/home-0/sutcliff/CASC/23/Problems/FEQ/FEQ061.p',backward_box)).
fof(f32,plain,(
  addition(domain(sK1),backward_box(sK0,domain(sK2))) = one),
  inference(cnf_transformation,[],[f30])).
fof(f209,plain,(
  ( ! [X4,X5] : (multiplication(X4,multiplication(coantidomain(X4),X5)) = zero) )),
  inference(forward_demodulation,[],[f197,f38])).
fof(f38,plain,(
  ( ! [X0] : (multiplication(zero,X0) = zero) )),
  inference(cnf_transformation,[],[f5])).
fof(f5,axiom,(
  ! [X0] : multiplication(zero,X0) = zero),
  file('/CW/home-0/sutcliff/CASC/23/Problems/FEQ/FEQ061.p',left_annihilation)).
fof(f197,plain,(
  ( ! [X4,X5] : (multiplication(zero,X5) = multiplication(X4,multiplication(coantidomain(X4),X5))) )),
  inference(superposition,[],[f58,f40])).
fof(f2009,plain,(
  ( ! [X0,X1] : (multiplication(X0,X1) = multiplication(X0,multiplication(coantidomain(coantidomain(X0)),X1))) )),
  inference(superposition,[],[f58,f1983])).
fof(f963073,plain,(
  ( ! [X707,X708] : (antidomain(X707) = antidomain(multiplication(X707,addition(X708,antidomain(X708))))) )),
  inference(forward_demodulation,[],[f963072,f567601])).
fof(f567601,plain,(
  ( ! [X354,X353] : (addition(antidomain(X353),antidomain(multiplication(X353,X354))) = antidomain(multiplication(X353,X354))) )),
  inference(forward_demodulation,[],[f567600,f47])).
fof(f567600,plain,(
  ( ! [X354,X353] : (addition(antidomain(multiplication(X353,X354)),antidomain(X353)) = antidomain(multiplication(X353,X354))) )),
  inference(forward_demodulation,[],[f567599,f37])).
fof(f567599,plain,(
  ( ! [X354,X353] : (multiplication(one,antidomain(multiplication(X353,X354))) = addition(antidomain(multiplication(X353,X354)),antidomain(X353))) )),
  inference(forward_demodulation,[],[f567598,f187])).
fof(f567598,plain,(
  ( ! [X354,X353] : (multiplication(addition(one,antidomain(X353)),antidomain(multiplication(X353,X354))) = addition(antidomain(multiplication(X353,X354)),antidomain(X353))) )),
  inference(forward_demodulation,[],[f567080,f3529])).
fof(f567080,plain,(
  ( ! [X354,X353] : (multiplication(addition(antidomain(X353),one),antidomain(multiplication(X353,X354))) = addition(antidomain(multiplication(X353,X354)),antidomain(X353))) )),
  inference(superposition,[],[f3510,f560701])).
fof(f560701,plain,(
  ( ! [X2,X1] : (multiplication(antidomain(X1),antidomain(multiplication(X1,X2))) = antidomain(X1)) )),
  inference(superposition,[],[f559592,f3762])).
fof(f3762,plain,(
  ( ! [X0,X1] : (multiplication(X0,X1) = multiplication(antidomain(antidomain(X0)),multiplication(X0,X1))) )),
  inference(superposition,[],[f58,f3719])).
fof(f559592,plain,(
  ( ! [X107,X106] : (multiplication(antidomain(X106),antidomain(multiplication(antidomain(antidomain(X106)),X107))) = antidomain(X106)) )),
  inference(superposition,[],[f558955,f41699])).
fof(f41699,plain,(
  ( ! [X39] : (antidomain(antidomain(X39)) = coantidomain(antidomain(X39))) )),
  inference(forward_demodulation,[],[f41698,f8996])).
fof(f8996,plain,(
  ( ! [X20] : (addition(antidomain(antidomain(X20)),coantidomain(antidomain(X20))) = antidomain(antidomain(X20))) )),
  inference(forward_demodulation,[],[f8995,f35])).
fof(f8995,plain,(
  ( ! [X20] : (multiplication(antidomain(antidomain(X20)),one) = addition(antidomain(antidomain(X20)),coantidomain(antidomain(X20)))) )),
  inference(forward_demodulation,[],[f8967,f188])).
fof(f8967,plain,(
  ( ! [X20] : (multiplication(antidomain(antidomain(X20)),addition(one,coantidomain(antidomain(X20)))) = addition(antidomain(antidomain(X20)),coantidomain(antidomain(X20)))) )),
  inference(superposition,[],[f1860,f8767])).
fof(f8767,plain,(
  ( ! [X62] : (multiplication(antidomain(antidomain(X62)),coantidomain(antidomain(X62))) = coantidomain(antidomain(X62))) )),
  inference(forward_demodulation,[],[f8686,f37])).
fof(f8686,plain,(
  ( ! [X62] : (multiplication(one,coantidomain(antidomain(X62))) = multiplication(antidomain(antidomain(X62)),coantidomain(antidomain(X62)))) )),
  inference(superposition,[],[f3541,f71])).
fof(f3541,plain,(
  ( ! [X28,X29] : (multiplication(X29,coantidomain(X28)) = multiplication(addition(X28,X29),coantidomain(X28))) )),
  inference(forward_demodulation,[],[f3452,f80])).
fof(f3452,plain,(
  ( ! [X28,X29] : (multiplication(addition(X28,X29),coantidomain(X28)) = addition(zero,multiplication(X29,coantidomain(X28)))) )),
  inference(superposition,[],[f60,f40])).
fof(f1860,plain,(
  ( ! [X12,X13] : (multiplication(X12,addition(one,X13)) = addition(X12,multiplication(X12,X13))) )),
  inference(superposition,[],[f59,f35])).
fof(f41698,plain,(
  ( ! [X39] : (addition(antidomain(antidomain(X39)),coantidomain(antidomain(X39))) = coantidomain(antidomain(X39))) )),
  inference(forward_demodulation,[],[f41697,f47])).
fof(f41697,plain,(
  ( ! [X39] : (addition(coantidomain(antidomain(X39)),antidomain(antidomain(X39))) = coantidomain(antidomain(X39))) )),
  inference(forward_demodulation,[],[f41696,f35])).
fof(f41696,plain,(
  ( ! [X39] : (multiplication(coantidomain(antidomain(X39)),one) = addition(coantidomain(antidomain(X39)),antidomain(antidomain(X39)))) )),
  inference(forward_demodulation,[],[f41643,f187])).
fof(f41643,plain,(
  ( ! [X39] : (multiplication(coantidomain(antidomain(X39)),addition(one,antidomain(antidomain(X39)))) = addition(coantidomain(antidomain(X39)),antidomain(antidomain(X39)))) )),
  inference(superposition,[],[f1860,f38526])).
fof(f38526,plain,(
  ( ! [X20] : (multiplication(coantidomain(antidomain(X20)),antidomain(antidomain(X20))) = antidomain(antidomain(X20))) )),
  inference(superposition,[],[f38401,f4813])).
fof(f38401,plain,(
  ( ! [X11] : (multiplication(coantidomain(antidomain(X11)),X11) = X11) )),
  inference(forward_demodulation,[],[f38311,f37])).
fof(f38311,plain,(
  ( ! [X11] : (multiplication(one,X11) = multiplication(coantidomain(antidomain(X11)),X11)) )),
  inference(superposition,[],[f7374,f72])).
fof(f7374,plain,(
  ( ! [X10,X11] : (multiplication(X11,X10) = multiplication(addition(X11,coantidomain(coantidomain(antidomain(X10)))),X10)) )),
  inference(forward_demodulation,[],[f7318,f34])).
fof(f7318,plain,(
  ( ! [X10,X11] : (multiplication(addition(X11,coantidomain(coantidomain(antidomain(X10)))),X10) = addition(multiplication(X11,X10),zero)) )),
  inference(superposition,[],[f60,f7274])).
fof(f7274,plain,(
  ( ! [X7] : (multiplication(coantidomain(coantidomain(antidomain(X7))),X7) = zero) )),
  inference(forward_demodulation,[],[f7212,f35])).
fof(f7212,plain,(
  ( ! [X7] : (multiplication(multiplication(coantidomain(coantidomain(antidomain(X7))),X7),one) = zero) )),
  inference(superposition,[],[f40,f7059])).
fof(f7059,plain,(
  ( ! [X54] : (one = coantidomain(multiplication(coantidomain(coantidomain(antidomain(X54))),X54))) )),
  inference(forward_demodulation,[],[f7058,f188])).
fof(f7058,plain,(
  ( ! [X54] : (addition(one,coantidomain(multiplication(coantidomain(coantidomain(antidomain(X54))),X54))) = coantidomain(multiplication(coantidomain(coantidomain(antidomain(X54))),X54))) )),
  inference(forward_demodulation,[],[f6930,f119])).
fof(f119,plain,(
  one = coantidomain(zero)),
  inference(forward_demodulation,[],[f117,f80])).
fof(f117,plain,(
  addition(zero,coantidomain(zero)) = one),
  inference(superposition,[],[f72,f74])).
fof(f74,plain,(
  zero = coantidomain(one)),
  inference(superposition,[],[f40,f37])).
fof(f6930,plain,(
  ( ! [X54] : (addition(coantidomain(zero),coantidomain(multiplication(coantidomain(coantidomain(antidomain(X54))),X54))) = coantidomain(multiplication(coantidomain(coantidomain(antidomain(X54))),X54))) )),
  inference(superposition,[],[f53,f41])).
fof(f53,plain,(
  ( ! [X0,X1] : (addition(coantidomain(multiplication(X0,X1)),coantidomain(multiplication(coantidomain(coantidomain(X0)),X1))) = coantidomain(multiplication(coantidomain(coantidomain(X0)),X1))) )),
  inference(cnf_transformation,[],[f17])).
fof(f17,axiom,(
  ! [X0,X1] : addition(coantidomain(multiplication(X0,X1)),coantidomain(multiplication(coantidomain(coantidomain(X0)),X1))) = coantidomain(multiplication(coantidomain(coantidomain(X0)),X1))),
  file('/CW/home-0/sutcliff/CASC/23/Problems/FEQ/FEQ061.p',codomain2)).
fof(f558955,plain,(
  ( ! [X2,X3] : (multiplication(X2,antidomain(multiplication(coantidomain(X2),X3))) = X2) )),
  inference(forward_demodulation,[],[f558954,f4813])).
fof(f558954,plain,(
  ( ! [X2,X3] : (multiplication(X2,antidomain(antidomain(antidomain(multiplication(coantidomain(X2),X3))))) = X2) )),
  inference(forward_demodulation,[],[f558078,f35])).
fof(f558078,plain,(
  ( ! [X2,X3] : (multiplication(X2,one) = multiplication(X2,antidomain(antidomain(antidomain(multiplication(coantidomain(X2),X3)))))) )),
  inference(superposition,[],[f11404,f71])).
fof(f11404,plain,(
  ( ! [X10,X11,X9] : (multiplication(X9,X11) = multiplication(X9,addition(antidomain(antidomain(multiplication(coantidomain(X9),X10))),X11))) )),
  inference(forward_demodulation,[],[f11256,f80])).
fof(f11256,plain,(
  ( ! [X10,X11,X9] : (multiplication(X9,addition(antidomain(antidomain(multiplication(coantidomain(X9),X10))),X11)) = addition(zero,multiplication(X9,X11))) )),
  inference(superposition,[],[f59,f11153])).
fof(f11153,plain,(
  ( ! [X12,X11] : (multiplication(X11,antidomain(antidomain(multiplication(coantidomain(X11),X12)))) = zero) )),
  inference(forward_demodulation,[],[f10972,f37])).
fof(f10972,plain,(
  ( ! [X12,X11] : (multiplication(one,multiplication(X11,antidomain(antidomain(multiplication(coantidomain(X11),X12))))) = zero) )),
  inference(superposition,[],[f41,f9786])).
fof(f9786,plain,(
  ( ! [X0,X1] : (one = antidomain(multiplication(X0,antidomain(antidomain(multiplication(coantidomain(X0),X1)))))) )),
  inference(forward_demodulation,[],[f9785,f187])).
fof(f9785,plain,(
  ( ! [X0,X1] : (addition(one,antidomain(multiplication(X0,antidomain(antidomain(multiplication(coantidomain(X0),X1)))))) = antidomain(multiplication(X0,antidomain(antidomain(multiplication(coantidomain(X0),X1)))))) )),
  inference(forward_demodulation,[],[f9625,f111])).
fof(f111,plain,(
  one = antidomain(zero)),
  inference(forward_demodulation,[],[f109,f80])).
fof(f109,plain,(
  addition(zero,antidomain(zero)) = one),
  inference(superposition,[],[f71,f77])).
fof(f77,plain,(
  zero = antidomain(one)),
  inference(superposition,[],[f41,f35])).
fof(f9625,plain,(
  ( ! [X0,X1] : (addition(antidomain(zero),antidomain(multiplication(X0,antidomain(antidomain(multiplication(coantidomain(X0),X1)))))) = antidomain(multiplication(X0,antidomain(antidomain(multiplication(coantidomain(X0),X1)))))) )),
  inference(superposition,[],[f54,f209])).
fof(f54,plain,(
  ( ! [X0,X1] : (addition(antidomain(multiplication(X0,X1)),antidomain(multiplication(X0,antidomain(antidomain(X1))))) = antidomain(multiplication(X0,antidomain(antidomain(X1))))) )),
  inference(cnf_transformation,[],[f18])).
fof(f18,axiom,(
  ! [X0,X1] : addition(antidomain(multiplication(X0,X1)),antidomain(multiplication(X0,antidomain(antidomain(X1))))) = antidomain(multiplication(X0,antidomain(antidomain(X1))))),
  file('/CW/home-0/sutcliff/CASC/23/Problems/FEQ/FEQ061.p',domain2)).
fof(f963072,plain,(
  ( ! [X707,X708] : (addition(antidomain(X707),antidomain(multiplication(X707,addition(X708,antidomain(X708))))) = antidomain(X707)) )),
  inference(forward_demodulation,[],[f963071,f4813])).
fof(f963071,plain,(
  ( ! [X707,X708] : (addition(antidomain(X707),antidomain(antidomain(antidomain(multiplication(X707,addition(X708,antidomain(X708))))))) = antidomain(X707)) )),
  inference(forward_demodulation,[],[f962790,f47])).
fof(f962790,plain,(
  ( ! [X707,X708] : (addition(antidomain(antidomain(antidomain(multiplication(X707,addition(X708,antidomain(X708)))))),antidomain(X707)) = antidomain(X707)) )),
  inference(superposition,[],[f567601,f961765])).
fof(f961765,plain,(
  ( ! [X2,X3] : (multiplication(antidomain(antidomain(multiplication(X2,addition(X3,antidomain(X3))))),X2) = X2) )),
  inference(forward_demodulation,[],[f961136,f37])).
fof(f961136,plain,(
  ( ! [X2,X3] : (multiplication(one,X2) = multiplication(antidomain(antidomain(multiplication(X2,addition(X3,antidomain(X3))))),X2)) )),
  inference(superposition,[],[f3545,f583091])).
fof(f583091,plain,(
  ( ! [X584,X585] : (addition(antidomain(X585),antidomain(antidomain(multiplication(X585,addition(X584,antidomain(X584)))))) = one) )),
  inference(forward_demodulation,[],[f583090,f35])).
fof(f583090,plain,(
  ( ! [X584,X585] : (addition(antidomain(multiplication(X585,one)),antidomain(antidomain(multiplication(X585,addition(X584,antidomain(X584)))))) = one) )),
  inference(forward_demodulation,[],[f583089,f111])).
fof(f583089,plain,(
  ( ! [X584,X585] : (addition(antidomain(multiplication(X585,antidomain(zero))),antidomain(antidomain(multiplication(X585,addition(X584,antidomain(X584)))))) = one) )),
  inference(forward_demodulation,[],[f582686,f47])).
fof(f582686,plain,(
  ( ! [X584,X585] : (addition(antidomain(antidomain(multiplication(X585,addition(X584,antidomain(X584))))),antidomain(multiplication(X585,antidomain(zero)))) = one) )),
  inference(superposition,[],[f61449,f582272])).
fof(f582272,plain,(
  ( ! [X0] : (zero = antidomain(addition(X0,antidomain(X0)))) )),
  inference(forward_demodulation,[],[f581903,f562972])).
fof(f562972,plain,(
  ( ! [X80,X79] : (antidomain(addition(X79,X80)) = antidomain(addition(X80,X79))) )),
  inference(forward_demodulation,[],[f562359,f561284])).
fof(f561284,plain,(
  ( ! [X265,X266] : (antidomain(X265) = antidomain(multiplication(X265,addition(one,X266)))) )),
  inference(backward_demodulation,[],[f560701,f102213])).
fof(f102213,plain,(
  ( ! [X265,X266] : (multiplication(antidomain(X265),antidomain(multiplication(X265,addition(one,X266)))) = antidomain(multiplication(X265,addition(one,X266)))) )),
  inference(forward_demodulation,[],[f101956,f4813])).
fof(f101956,plain,(
  ( ! [X265,X266] : (multiplication(antidomain(antidomain(antidomain(X265))),antidomain(multiplication(X265,addition(one,X266)))) = antidomain(multiplication(X265,addition(one,X266)))) )),
  inference(superposition,[],[f63094,f9766])).
fof(f9766,plain,(
  ( ! [X14,X13] : (addition(antidomain(X14),antidomain(multiplication(X14,addition(one,X13)))) = antidomain(X14)) )),
  inference(forward_demodulation,[],[f9765,f35])).
fof(f9765,plain,(
  ( ! [X14,X13] : (addition(antidomain(multiplication(X14,one)),antidomain(multiplication(X14,addition(one,X13)))) = antidomain(multiplication(X14,one))) )),
  inference(forward_demodulation,[],[f9764,f111])).
fof(f9764,plain,(
  ( ! [X14,X13] : (addition(antidomain(multiplication(X14,antidomain(zero))),antidomain(multiplication(X14,addition(one,X13)))) = antidomain(multiplication(X14,antidomain(zero)))) )),
  inference(forward_demodulation,[],[f9617,f47])).
fof(f9617,plain,(
  ( ! [X14,X13] : (addition(antidomain(multiplication(X14,addition(one,X13))),antidomain(multiplication(X14,antidomain(zero)))) = antidomain(multiplication(X14,antidomain(zero)))) )),
  inference(superposition,[],[f54,f2536])).
fof(f2536,plain,(
  ( ! [X9] : (zero = antidomain(addition(one,X9))) )),
  inference(superposition,[],[f2486,f35])).
fof(f2486,plain,(
  ( ! [X8,X9] : (multiplication(antidomain(addition(X8,X9)),X8) = zero) )),
  inference(forward_demodulation,[],[f2485,f1930])).
fof(f2485,plain,(
  ( ! [X8,X9] : (multiplication(antidomain(addition(X8,X9)),addition(X8,addition(X8,X9))) = zero) )),
  inference(forward_demodulation,[],[f2400,f1915])).
fof(f1915,plain,(
  ( ! [X6,X7,X5] : (multiplication(X5,addition(X6,X7)) = multiplication(X5,addition(X7,X6))) )),
  inference(forward_demodulation,[],[f1869,f59])).
fof(f1869,plain,(
  ( ! [X6,X7,X5] : (multiplication(X5,addition(X6,X7)) = addition(multiplication(X5,X7),multiplication(X5,X6))) )),
  inference(superposition,[],[f59,f47])).
fof(f2400,plain,(
  ( ! [X8,X9] : (multiplication(antidomain(addition(X8,X9)),addition(addition(X8,X9),X8)) = zero) )),
  inference(superposition,[],[f2270,f143])).
fof(f2270,plain,(
  ( ! [X21,X20] : (multiplication(antidomain(addition(X20,X21)),addition(X21,X20)) = zero) )),
  inference(superposition,[],[f1915,f41])).
fof(f63094,plain,(
  ( ! [X2,X1] : (multiplication(antidomain(antidomain(addition(X2,X1))),X1) = X1) )),
  inference(superposition,[],[f62962,f47])).
fof(f62962,plain,(
  ( ! [X0,X1] : (multiplication(antidomain(antidomain(addition(X0,X1))),X0) = X0) )),
  inference(forward_demodulation,[],[f62839,f37])).
fof(f62839,plain,(
  ( ! [X0,X1] : (multiplication(one,X0) = multiplication(antidomain(antidomain(addition(X0,X1))),X0)) )),
  inference(superposition,[],[f3551,f71])).
fof(f3551,plain,(
  ( ! [X59,X60,X58] : (multiplication(X60,X58) = multiplication(addition(antidomain(addition(X58,X59)),X60),X58)) )),
  inference(forward_demodulation,[],[f3463,f80])).
fof(f3463,plain,(
  ( ! [X59,X60,X58] : (multiplication(addition(antidomain(addition(X58,X59)),X60),X58) = addition(zero,multiplication(X60,X58))) )),
  inference(superposition,[],[f60,f2486])).
fof(f562359,plain,(
  ( ! [X80,X81,X79] : (antidomain(addition(X79,X80)) = antidomain(multiplication(addition(X80,X79),addition(one,X81)))) )),
  inference(superposition,[],[f561284,f3529])).
fof(f581903,plain,(
  ( ! [X0] : (zero = antidomain(addition(antidomain(X0),X0))) )),
  inference(superposition,[],[f560706,f16503])).
fof(f16503,plain,(
  ( ! [X2,X1] : (multiplication(antidomain(addition(X2,X1)),antidomain(antidomain(X1))) = zero) )),
  inference(superposition,[],[f16432,f47])).
fof(f16432,plain,(
  ( ! [X10,X9] : (multiplication(antidomain(addition(X9,X10)),antidomain(antidomain(X9))) = zero) )),
  inference(forward_demodulation,[],[f16320,f37])).
fof(f16320,plain,(
  ( ! [X10,X9] : (multiplication(one,multiplication(antidomain(addition(X9,X10)),antidomain(antidomain(X9)))) = zero) )),
  inference(superposition,[],[f41,f9856])).
fof(f9856,plain,(
  ( ! [X94,X93] : (one = antidomain(multiplication(antidomain(addition(X93,X94)),antidomain(antidomain(X93))))) )),
  inference(forward_demodulation,[],[f9855,f187])).
fof(f9855,plain,(
  ( ! [X94,X93] : (addition(one,antidomain(multiplication(antidomain(addition(X93,X94)),antidomain(antidomain(X93))))) = antidomain(multiplication(antidomain(addition(X93,X94)),antidomain(antidomain(X93))))) )),
  inference(forward_demodulation,[],[f9671,f111])).
fof(f9671,plain,(
  ( ! [X94,X93] : (addition(antidomain(zero),antidomain(multiplication(antidomain(addition(X93,X94)),antidomain(antidomain(X93))))) = antidomain(multiplication(antidomain(addition(X93,X94)),antidomain(antidomain(X93))))) )),
  inference(superposition,[],[f54,f2486])).
fof(f560706,plain,(
  ( ! [X10,X9] : (multiplication(antidomain(addition(X9,X10)),antidomain(X9)) = antidomain(addition(X9,X10))) )),
  inference(superposition,[],[f559592,f62962])).
fof(f61449,plain,(
  ( ! [X4,X3] : (addition(antidomain(antidomain(multiplication(X3,X4))),antidomain(multiplication(X3,antidomain(antidomain(X4))))) = one) )),
  inference(forward_demodulation,[],[f61448,f47])).
fof(f61448,plain,(
  ( ! [X4,X3] : (addition(antidomain(multiplication(X3,antidomain(antidomain(X4)))),antidomain(antidomain(multiplication(X3,X4)))) = one) )),
  inference(forward_demodulation,[],[f61447,f187])).
fof(f61447,plain,(
  ( ! [X4,X3] : (addition(one,antidomain(multiplication(X3,antidomain(antidomain(X4))))) = addition(antidomain(multiplication(X3,antidomain(antidomain(X4)))),antidomain(antidomain(multiplication(X3,X4))))) )),
  inference(forward_demodulation,[],[f61143,f47])).
fof(f61143,plain,(
  ( ! [X4,X3] : (addition(antidomain(multiplication(X3,antidomain(antidomain(X4)))),one) = addition(antidomain(multiplication(X3,antidomain(antidomain(X4)))),antidomain(antidomain(multiplication(X3,X4))))) )),
  inference(superposition,[],[f9721,f684])).
fof(f684,plain,(
  ( ! [X54,X55] : (addition(X55,one) = addition(antidomain(X54),addition(X55,antidomain(antidomain(X54))))) )),
  inference(superposition,[],[f160,f71])).
fof(f160,plain,(
  ( ! [X6,X4,X5] : (addition(X4,addition(X5,X6)) = addition(X5,addition(X4,X6))) )),
  inference(forward_demodulation,[],[f144,f57])).
fof(f144,plain,(
  ( ! [X6,X4,X5] : (addition(X4,addition(X5,X6)) = addition(addition(X5,X4),X6)) )),
  inference(superposition,[],[f57,f47])).
fof(f9721,plain,(
  ( ! [X14,X15,X16] : (addition(antidomain(multiplication(X14,antidomain(antidomain(X15)))),X16) = addition(antidomain(multiplication(X14,X15)),addition(antidomain(multiplication(X14,antidomain(antidomain(X15)))),X16))) )),
  inference(superposition,[],[f57,f54])).
fof(f1745491,plain,(
  ( ! [X0,X1] : (addition(antidomain(antidomain(X0)),antidomain(multiplication(antidomain(X1),X0))) = one) )),
  inference(forward_demodulation,[],[f1743185,f47])).
fof(f1743185,plain,(
  ( ! [X0,X1] : (addition(antidomain(multiplication(antidomain(X1),X0)),antidomain(antidomain(X0))) = one) )),
  inference(superposition,[],[f1733666,f36])).
fof(f1733666,plain,(
  ( ! [X356,X358,X357] : (addition(antidomain(multiplication(antidomain(X357),X356)),antidomain(antidomain(addition(X356,X358)))) = one) )),
  inference(superposition,[],[f674215,f1732120])).
fof(f1732120,plain,(
  ( ! [X80,X81,X82] : (addition(X81,X82) = addition(X81,addition(multiplication(antidomain(X80),X81),X82))) )),
  inference(forward_demodulation,[],[f1728251,f37])).
fof(f1728251,plain,(
  ( ! [X80,X81,X82] : (addition(multiplication(one,X81),X82) = addition(X81,addition(multiplication(antidomain(X80),X81),X82))) )),
  inference(superposition,[],[f29325,f187])).
fof(f29325,plain,(
  ( ! [X261,X260,X262] : (addition(multiplication(addition(one,X261),X260),X262) = addition(X260,addition(multiplication(X261,X260),X262))) )),
  inference(superposition,[],[f3476,f37])).
fof(f3476,plain,(
  ( ! [X17,X15,X18,X16] : (addition(multiplication(addition(X15,X17),X16),X18) = addition(multiplication(X15,X16),addition(multiplication(X17,X16),X18))) )),
  inference(superposition,[],[f57,f60])).
fof(f674215,plain,(
  ( ! [X492,X490,X491] : (addition(antidomain(X491),antidomain(antidomain(addition(X490,addition(X491,X492))))) = one) )),
  inference(forward_demodulation,[],[f673015,f47])).
fof(f673015,plain,(
  ( ! [X492,X490,X491] : (addition(antidomain(antidomain(addition(X490,addition(X491,X492)))),antidomain(X491)) = one) )),
  inference(superposition,[],[f668589,f63101])).
fof(f63101,plain,(
  ( ! [X14,X15,X16] : (multiplication(antidomain(antidomain(addition(X16,addition(X14,X15)))),X14) = X14) )),
  inference(superposition,[],[f62962,f152])).
fof(f152,plain,(
  ( ! [X8,X7,X9] : (addition(X7,addition(X8,X9)) = addition(X9,addition(X7,X8))) )),
  inference(superposition,[],[f57,f47])).
fof(f668589,plain,(
  ( ! [X74,X75] : (addition(antidomain(X74),antidomain(multiplication(antidomain(X74),X75))) = one) )),
  inference(forward_demodulation,[],[f667098,f187])).
fof(f667098,plain,(
  ( ! [X74,X75] : (addition(one,antidomain(multiplication(antidomain(X74),X75))) = addition(antidomain(X74),antidomain(multiplication(antidomain(X74),X75)))) )),
  inference(superposition,[],[f148,f567601])).
fof(f148,plain,(
  ( ! [X17,X16] : (addition(one,X17) = addition(antidomain(X16),addition(antidomain(antidomain(X16)),X17))) )),
  inference(superposition,[],[f57,f71])).
% SZS output end Proof for FEQ061
------------------------------
Version: Vampire 1.0 (revision 700)
Termination reason: Refutation

Active clauses: 1814
Passive clauses: 24349
Generated clauses: 1751841
Final active clauses: 1577
Final passive clauses: 4836
Input formulas: 27
Initial clauses: 22
Discarded non-redundant clauses: 371022

Function definitions: 8
Splitted inequalities: 1

Trivial inequalities: 63
Fw subsumption resolutions: 1
Fw demodulations: 723414
Bw demodulations: 3839
Fw literal rewrites: 139

Simple tautologies: 502
Forward subsumptions: 627405
Fw demodulations to eq. taut.: 17572
Bw demodulations to eq. taut.: 1220

Binary resolution: 75
Forward superposition: 519495
Backward superposition: 504043
Self superposition: 750

Memory used: 970602KB
Time elapsed: 33.703 s
------------------------------
% Success in time 40.61 s

WATCH: 40.57 CPU 40.66 WC

FINAL WATCH: 40.57 CPU 40.66 WC