% 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: 33
dis+1_6_bd=off:bs=off:lcm=predicate:nwc=1.5:nicw=on:sswsr=on:ss=included:st=1.5:sac=on:sp=occurrence_24 on FEQ073

WATCH: 0.00 CPU 0.01 WC

WATCH: 2.99 CPU 3.02 WC
Time limit reached!
------------------------------
Version: Vampire 1.0 (revision 700)
Termination reason: Time limit

Active clauses: 476
Passive clauses: 42151
Generated clauses: 95348
Final active clauses: 476
Final passive clauses: 40540
Input formulas: 17
Initial clauses: 15

Selected by SInE selection: 14
SInE iterations: 3

Trivial inequalities: 242
Fw subsumption resolutions: 319
Fw demodulations: 38038

Simple tautologies: 213
Forward subsumptions: 15069
Fw demodulations to eq. taut.: 451

Binary resolution: 472
Forward superposition: 27173
Backward superposition: 29044
Self superposition: 217

Unique components: 15

Memory used: 130360KB
Time elapsed: 3.412 s
------------------------------
% remaining time: 2965 next slice time: 29
lrs+11_40_bd=off:bs=unit_only:bsr=unit_only:drc=off:flr=on:lcm=predicate:nwc=1:ptb=off:ssec=off:stl=60:sac=on:spl=backtracking:sfv=off:updr=off_21 on FEQ073

WATCH: 6.00 CPU 6.03 WC
Time limit reached!
------------------------------
Version: Vampire 1.0 (revision 700)
Termination reason: Time limit

Active clauses: 273
Passive clauses: 5040
Generated clauses: 60318
Final active clauses: 251
Final passive clauses: 4634
Input formulas: 17
Initial clauses: 18

Trivial inequalities: 290
Fw subsumption resolutions: 106
Fw demodulations: 34057
Fw literal rewrites: 59

Simple tautologies: 1675
Forward subsumptions: 17945
Backward subsumptions: 155
Fw demodulations to eq. taut.: 1146

Binary resolution: 322
Forward superposition: 14596
Backward superposition: 11573
Self superposition: 161
Equality resolution: 2

Memory used: 107333KB
Time elapsed: 3.111 s
------------------------------
% remaining time: 2934 next slice time: 229
lrs+10_7_bd=off:bs=unit_only:bsr=unit_only:drc=off:ep=on:flr=on:fde=none:lcm=predicate:nwc=1.7:ptb=off:ssec=off:stl=60:sagn=off:sgo=on:spo=on:spl=backtracking:sp=reverse_arity:updr=off_169 on FEQ073

WATCH: 8.98 CPU 9.05 WC

WATCH: 12.01 CPU 12.06 WC

WATCH: 15.02 CPU 15.07 WC

WATCH: 18.04 CPU 18.08 WC

WATCH: 21.04 CPU 21.09 WC

WATCH: 24.05 CPU 24.10 WC

WATCH: 27.07 CPU 27.11 WC
Time limit reached!
------------------------------
Version: Vampire 1.0 (revision 700)
Termination reason: Time limit

Active clauses: 1019
Passive clauses: 21301
Generated clauses: 603496
Final active clauses: 997
Final passive clauses: 13302
Input formulas: 17
Initial clauses: 18
Discarded non-redundant clauses: 264270

Trivial inequalities: 2242
Fw subsumption resolutions: 439
Fw demodulations: 200998
Fw literal rewrites: 614

Simple tautologies: 6586
Forward subsumptions: 116705
Backward subsumptions: 294
Fw demodulations to eq. taut.: 8095

Binary resolution: 2218
Forward superposition: 221819
Backward superposition: 175299
Self superposition: 594
Equality resolution: 2

Memory used: 553551KB
Time elapsed: 23.145 s
------------------------------
% remaining time: 2702 next slice time: 134
dis+1003_2_bsr=unit_only:bms=on:cond=fast:flr=on:fde=none:gsp=input_only:nwc=1.5:ssec=off:sac=on:sfv=off:sp=reverse_arity:updr=off_99 on FEQ073

WATCH: 30.09 CPU 30.13 WC

WATCH: 33.08 CPU 33.14 WC

WATCH: 36.10 CPU 36.15 WC

WATCH: 39.11 CPU 39.16 WC

WATCH: 42.11 CPU 42.16 WC
Time limit reached!
------------------------------
Version: Vampire 1.0 (revision 700)
Termination reason: Time limit

Active clauses: 434
Passive clauses: 85847
Generated clauses: 222873
Final active clauses: 394
Final passive clauses: 84123
Input formulas: 17
Initial clauses: 18

Trivial inequalities: 491
Fw subsumption resolutions: 403
Fw demodulations: 115063
Bw demodulations: 29
Fw literal rewrites: 709

Simple tautologies: 512
Forward subsumptions: 19241
Backward subsumptions: 11
Fw demodulations to eq. taut.: 1897

Binary resolution: 474
Forward superposition: 56631
Backward superposition: 49896
Self superposition: 365
Equality resolution: 5

Unique components: 14

Memory used: 527837KB
Time elapsed: 13.717 s
------------------------------
% remaining time: 2564 next slice time: 4
lrs-1_5_bd=off:drc=off:lcm=predicate:nwc=1.5:nicw=on:ptb=off:ssec=off:stl=60:sagn=off:spl=backtracking:sp=occurrence:updr=off_2 on FEQ073
Time limit reached!
------------------------------
Version: Vampire 1.0 (revision 700)
Termination reason: Time limit

Active clauses: 171
Passive clauses: 1143
Generated clauses: 12558
Final active clauses: 161
Final passive clauses: 955
Input formulas: 17
Initial clauses: 18

Trivial inequalities: 40
Fw subsumption resolutions: 79
Fw demodulations: 6980

Simple tautologies: 64
Equational tautologies: 2
Forward subsumptions: 4014
Backward subsumptions: 27
Fw demodulations to eq. taut.: 236

Binary resolution: 355
Forward superposition: 3121
Backward superposition: 1903
Self superposition: 70
Equality resolution: 5

Memory used: 17014KB
Time elapsed: 0.590 s
------------------------------
% remaining time: 2558 next slice time: 203
lrs+1011_1_bs=off:bsr=unit_only:drc=off:flr=on:fsr=off:gsp=input_only:nwc=1.5:nicw=on:ptb=off:ssec=off:stl=60:spl=backtracking_150 on FEQ073

WATCH: 45.09 CPU 45.17 WC

WATCH: 48.09 CPU 48.18 WC

WATCH: 51.10 CPU 51.19 WC

WATCH: 54.11 CPU 54.20 WC

WATCH: 57.13 CPU 57.21 WC

WATCH: 60.13 CPU 60.22 WC

WATCH: 63.15 CPU 63.23 WC
Time limit reached!
------------------------------
Version: Vampire 1.0 (revision 700)
Termination reason: Time limit

Active clauses: 535
Passive clauses: 28408
Generated clauses: 174589
Final active clauses: 502
Final passive clauses: 25696
Input formulas: 17
Initial clauses: 18
Discarded non-redundant clauses: 8612

Duplicate literals: 5
Trivial inequalities: 938
Fw demodulations: 75991
Bw demodulations: 745
Fw literal rewrites: 10831

Simple tautologies: 787
Forward subsumptions: 49909
Fw demodulations to eq. taut.: 1824
Bw demodulations to eq. taut.: 40

Binary resolution: 911
Forward superposition: 61275
Backward superposition: 23968
Self superposition: 315
Equality resolution: 2

Memory used: 525279KB
Time elapsed: 20.491 s
------------------------------
% remaining time: 2353 next slice time: 146
dis+3_64_bd=off:bs=unit_only:bsr=on:cond=on:ep=on:fde=none:gsp=input_only:nwc=10:nicw=on:ptb=off:ssec=off:sagn=off:sio=off:spl=backtracking:sfv=off:sp=occurrence:updr=off_108 on FEQ073

WATCH: 66.15 CPU 66.25 WC

WATCH: 69.17 CPU 69.26 WC

WATCH: 72.17 CPU 72.27 WC

WATCH: 75.19 CPU 75.29 WC

WATCH: 78.20 CPU 78.30 WC
Time limit reached!
------------------------------
Version: Vampire 1.0 (revision 700)
Termination reason: Time limit

Active clauses: 2104
Passive clauses: 199512
Generated clauses: 539091
Final active clauses: 1996
Final passive clauses: 185080
Input formulas: 17
Initial clauses: 18

Trivial inequalities: 269
Fw subsumption resolutions: 452
Fw demodulations: 181639

Simple tautologies: 629
Forward subsumptions: 167962
Backward subsumptions: 108
Fw demodulations to eq. taut.: 952

Binary resolution: 2903
Forward superposition: 211973
Backward superposition: 142776
Self superposition: 256
Equality resolution: 5

Backtracking splits: 4

Memory used: 536920KB
Time elapsed: 14.716 s
------------------------------
% remaining time: 2205 next slice time: 401
dis+10_1_bs=off:flr=on:gsp=input_only:lcm=predicate:sos=on:sp=reverse_arity:updr=off_297 on FEQ073
Refutation not found with incomplete strategy!
------------------------------
Version: Vampire 1.0 (revision 700)
Termination reason: Refutation not found, incomplete strategy

Active clauses: 19
Passive clauses: 3
Generated clauses: 4
Final active clauses: 19
Input formulas: 17
Initial clauses: 18

Fw literal rewrites: 1

Forward subsumptions: 1

Forward superposition: 2

Memory used: 127KB
Time elapsed: 0.0000 s
------------------------------
% remaining time: 2205 next slice time: 3
dis-2_4_bs=unit_only:bsr=on:cond=fast:drc=off:flr=on:lcm=predicate:nwc=2:nicw=on:ptb=off:ssec=off:sswsr=on:sagn=off:sio=off:spl=backtracking_1 on FEQ073
Time limit reached!
------------------------------
Version: Vampire 1.0 (revision 700)
Termination reason: Time limit

Active clauses: 304
Passive clauses: 5995
Generated clauses: 25266
Final active clauses: 153
Final passive clauses: 5128
Input formulas: 17
Initial clauses: 18

Duplicate literals: 146
Trivial inequalities: 332
Fw subsumption resolutions: 129
Bw subsumption resolutions: 100
Fw demodulations: 9736
Bw demodulations: 16
Fw literal rewrites: 93
Condensations: 680

Simple tautologies: 741
Forward subsumptions: 7731
Backward subsumptions: 8
Fw demodulations to eq. taut.: 122

Binary resolution: 398
Forward superposition: 5265
Backward superposition: 8610
Self superposition: 59
Equality resolution: 1

Backtracking splits: 31
Backtracking splits refuted: 27
Backtracking splits refuted at zero level: 26

Memory used: 11769KB
Time elapsed: 0.400 s
------------------------------
% remaining time: 2201 next slice time: 376
lrs-1004_32_fde=none:lcm=predicate:nwc=2.0:nicw=on:ptb=off:ssec=off:stl=60:sac=on:sio=off:spl=backtracking:sp=occurrence_278 on FEQ073

WATCH: 81.21 CPU 81.31 WC

WATCH: 84.21 CPU 84.32 WC

WATCH: 87.22 CPU 87.33 WC

WATCH: 90.23 CPU 90.34 WC
Refutation found. Thanks to Tanya!
% SZS status Theorem for FEQ073
% SZS output start Proof for FEQ073
fof(f430941,plain,(
  $false),
  inference(subsumption_resolution,[],[f430940,f52])).
fof(f52,plain,(
  ( ! [X0] : (leq(X0,X0)) )),
  inference(resolution,[],[f33,f26])).
fof(f26,plain,(
  ( ! [X0] : (addition(X0,X0) = X0) )),
  inference(cnf_transformation,[],[f13])).
fof(f13,axiom,(
  ! [X0] : addition(X0,X0) = X0),
  file('/CW/home-0/sutcliff/CASC/23/Problems/FEQ/FEQ073.p',additive_idempotence)).
fof(f33,plain,(
  ( ! [X0,X1] : (addition(X0,X1) != X1 | leq(X0,X1)) )),
  inference(cnf_transformation,[],[f22])).
fof(f22,plain,(
  ! [X0,X1] : ((addition(X0,X1) != X1 | leq(X0,X1)) & (~leq(X0,X1) | addition(X0,X1) = X1))),
  inference(nnf_transformation,[],[f9])).
fof(f9,axiom,(
  ! [X0,X1] : (addition(X0,X1) = X1 <=> leq(X0,X1))),
  file('/CW/home-0/sutcliff/CASC/23/Problems/FEQ/FEQ073.p',order)).
fof(f430940,plain,(
  ~leq(one,one)),
  inference(forward_demodulation,[],[f430939,f41])).
fof(f41,plain,(
  ( ! [X0] : (addition(zero,X0) = X0) )),
  inference(superposition,[],[f32,f25])).
fof(f25,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/FEQ073.p',additive_identity)).
fof(f32,plain,(
  ( ! [X0,X1] : (addition(X0,X1) = addition(X1,X0)) )),
  inference(cnf_transformation,[],[f16])).
fof(f16,axiom,(
  ! [X0,X1] : addition(X0,X1) = addition(X1,X0)),
  file('/CW/home-0/sutcliff/CASC/23/Problems/FEQ/FEQ073.p',additive_commutativity)).
fof(f430939,plain,(
  ~leq(addition(zero,one),one)),
  inference(forward_demodulation,[],[f430938,f32])).
fof(f430938,plain,(
  ~leq(addition(one,zero),one)),
  inference(forward_demodulation,[],[f430937,f97357])).
fof(f97357,plain,(
  ( ! [X14,X15] : (multiplication(addition(X15,X14),one) = addition(X14,X15)) )),
  inference(superposition,[],[f54940,f24])).
fof(f24,plain,(
  ( ! [X0] : (multiplication(X0,one) = X0) )),
  inference(cnf_transformation,[],[f12])).
fof(f12,axiom,(
  ! [X0] : multiplication(X0,one) = X0),
  file('/CW/home-0/sutcliff/CASC/23/Problems/FEQ/FEQ073.p',multiplicative_right_identity)).
fof(f54940,plain,(
  ( ! [X8,X7,X9] : (multiplication(addition(X7,X9),X8) = multiplication(addition(X9,X7),X8)) )),
  inference(superposition,[],[f6818,f38])).
fof(f38,plain,(
  ( ! [X2,X0,X1] : (multiplication(addition(X0,X1),X2) = addition(multiplication(X0,X2),multiplication(X1,X2))) )),
  inference(cnf_transformation,[],[f8])).
fof(f8,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/FEQ073.p',left_distributivity)).
fof(f6818,plain,(
  ( ! [X14,X15,X13] : (multiplication(addition(X13,X15),X14) = addition(multiplication(X15,X14),multiplication(X13,X14))) )),
  inference(superposition,[],[f38,f32])).
fof(f430937,plain,(
  ~leq(multiplication(addition(zero,one),one),one)),
  inference(forward_demodulation,[],[f430936,f54940])).
fof(f430936,plain,(
  ~leq(multiplication(addition(one,zero),one),one)),
  inference(forward_demodulation,[],[f430932,f6826])).
fof(f6826,plain,(
  ( ! [X17,X16] : (multiplication(addition(one,X17),X16) = addition(X16,multiplication(X17,X16))) )),
  inference(superposition,[],[f38,f27])).
fof(f27,plain,(
  ( ! [X0] : (multiplication(one,X0) = X0) )),
  inference(cnf_transformation,[],[f5])).
fof(f5,axiom,(
  ! [X0] : multiplication(one,X0) = X0),
  file('/CW/home-0/sutcliff/CASC/23/Problems/FEQ/FEQ073.p',multiplicative_left_identity)).
fof(f430932,plain,(
  ~leq(addition(one,multiplication(zero,one)),one)),
  inference(resolution,[],[f430929,f15230])).
fof(f15230,plain,(
  ( ! [X0,X1] : (leq(star(X0),X1) | ~leq(addition(one,multiplication(X0,X1)),X1)) )),
  inference(forward_demodulation,[],[f15221,f32])).
fof(f15221,plain,(
  ( ! [X0,X1] : (leq(star(X0),X1) | ~leq(addition(multiplication(X0,X1),one),X1)) )),
  inference(superposition,[],[f40,f24])).
fof(f40,plain,(
  ( ! [X2,X0,X1] : (leq(multiplication(star(X0),X2),X1) | ~leq(addition(multiplication(X0,X1),X2),X1)) )),
  inference(cnf_transformation,[],[f21])).
fof(f21,plain,(
  ! [X0,X1,X2] : (~leq(addition(multiplication(X0,X1),X2),X1) | leq(multiplication(star(X0),X2),X1))),
  inference(ennf_transformation,[],[f6])).
fof(f6,axiom,(
  ! [X0,X1,X2] : (leq(addition(multiplication(X0,X1),X2),X1) => leq(multiplication(star(X0),X2),X1))),
  file('/CW/home-0/sutcliff/CASC/23/Problems/FEQ/FEQ073.p',star_induction_left)).
fof(f430929,plain,(
  ~leq(star(zero),one)),
  inference(forward_demodulation,[],[f418628,f385373])).
fof(f385373,plain,(
  star(zero) = star(one)),
  inference(superposition,[],[f384457,f25])).
fof(f384457,plain,(
  ( ! [X2] : (star(X2) = star(addition(one,X2))) )),
  inference(forward_demodulation,[],[f384136,f173773])).
fof(f173773,plain,(
  ( ! [X1] : (addition(star(X1),star(addition(one,X1))) = star(X1)) )),
  inference(superposition,[],[f151737,f32])).
fof(f151737,plain,(
  ( ! [X34] : (addition(star(addition(one,X34)),star(X34)) = star(X34)) )),
  inference(subsumption_resolution,[],[f151736,f52])).
fof(f151736,plain,(
  ( ! [X34] : (~leq(star(X34),star(X34)) | addition(star(addition(one,X34)),star(X34)) = star(X34)) )),
  inference(forward_demodulation,[],[f151663,f44367])).
fof(f44367,plain,(
  ( ! [X201] : (addition(one,star(X201)) = star(X201)) )),
  inference(superposition,[],[f149,f44186])).
fof(f44186,plain,(
  ( ! [X1] : (addition(one,multiplication(addition(one,X1),star(X1))) = star(X1)) )),
  inference(forward_demodulation,[],[f43984,f6826])).
fof(f43984,plain,(
  ( ! [X1] : (addition(one,addition(star(X1),multiplication(X1,star(X1)))) = star(X1)) )),
  inference(superposition,[],[f89,f1759])).
fof(f1759,plain,(
  ( ! [X24,X23,X22] : (addition(addition(X23,X24),X22) = addition(X23,addition(X22,X24))) )),
  inference(superposition,[],[f596,f32])).
fof(f596,plain,(
  ( ! [X4,X2,X3] : (addition(X4,addition(X3,X2)) = addition(X3,addition(X4,X2))) )),
  inference(superposition,[],[f146,f32])).
fof(f146,plain,(
  ( ! [X8,X7,X9] : (addition(X9,addition(X7,X8)) = addition(X7,addition(X8,X9))) )),
  inference(superposition,[],[f35,f32])).
fof(f35,plain,(
  ( ! [X2,X0,X1] : (addition(addition(X2,X1),X0) = addition(X2,addition(X1,X0))) )),
  inference(cnf_transformation,[],[f18])).
fof(f18,plain,(
  ! [X0,X1,X2] : addition(addition(X2,X1),X0) = addition(X2,addition(X1,X0))),
  inference(rectify,[],[f7])).
fof(f7,axiom,(
  ! [X2,X1,X0] : addition(addition(X0,X1),X2) = addition(X0,addition(X1,X2))),
  file('/CW/home-0/sutcliff/CASC/23/Problems/FEQ/FEQ073.p',additive_associativity)).
fof(f89,plain,(
  ( ! [X0] : (addition(addition(one,multiplication(X0,star(X0))),star(X0)) = star(X0)) )),
  inference(resolution,[],[f30,f34])).
fof(f34,plain,(
  ( ! [X0,X1] : (~leq(X0,X1) | addition(X0,X1) = X1) )),
  inference(cnf_transformation,[],[f22])).
fof(f30,plain,(
  ( ! [X0] : (leq(addition(one,multiplication(X0,star(X0))),star(X0))) )),
  inference(cnf_transformation,[],[f10])).
fof(f10,axiom,(
  ! [X0] : leq(addition(one,multiplication(X0,star(X0))),star(X0))),
  file('/CW/home-0/sutcliff/CASC/23/Problems/FEQ/FEQ073.p',star_unfold_right)).
fof(f149,plain,(
  ( ! [X2,X3] : (addition(X2,X3) = addition(X2,addition(X2,X3))) )),
  inference(superposition,[],[f35,f26])).
fof(f151663,plain,(
  ( ! [X34] : (~leq(addition(one,star(X34)),star(X34)) | addition(star(addition(one,X34)),star(X34)) = star(X34)) )),
  inference(superposition,[],[f10200,f55438])).
fof(f55438,plain,(
  ( ! [X0] : (multiplication(star(X0),addition(one,X0)) = star(X0)) )),
  inference(superposition,[],[f54602,f32])).
fof(f54602,plain,(
  ( ! [X1] : (multiplication(star(X1),addition(X1,one)) = star(X1)) )),
  inference(superposition,[],[f46811,f2614])).
fof(f2614,plain,(
  ( ! [X0,X1] : (multiplication(X0,addition(X1,one)) = addition(multiplication(X0,X1),X0)) )),
  inference(superposition,[],[f37,f24])).
fof(f37,plain,(
  ( ! [X2,X0,X1] : (multiplication(X0,addition(X1,X2)) = addition(multiplication(X0,X1),multiplication(X0,X2))) )),
  inference(cnf_transformation,[],[f3])).
fof(f3,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/FEQ073.p',right_distributivity)).
fof(f46811,plain,(
  ( ! [X3] : (addition(multiplication(star(X3),X3),star(X3)) = star(X3)) )),
  inference(forward_demodulation,[],[f46810,f44367])).
fof(f46810,plain,(
  ( ! [X3] : (addition(multiplication(star(X3),X3),addition(one,star(X3))) = star(X3)) )),
  inference(forward_demodulation,[],[f46599,f32])).
fof(f46599,plain,(
  ( ! [X3] : (addition(multiplication(star(X3),X3),addition(star(X3),one)) = star(X3)) )),
  inference(superposition,[],[f123,f609])).
fof(f609,plain,(
  ( ! [X14,X12,X13] : (addition(X14,addition(X12,X13)) = addition(addition(X13,X14),X12)) )),
  inference(superposition,[],[f146,f32])).
fof(f123,plain,(
  ( ! [X0] : (addition(addition(one,multiplication(star(X0),X0)),star(X0)) = star(X0)) )),
  inference(resolution,[],[f31,f34])).
fof(f31,plain,(
  ( ! [X0] : (leq(addition(one,multiplication(star(X0),X0)),star(X0))) )),
  inference(cnf_transformation,[],[f4])).
fof(f4,axiom,(
  ! [X0] : leq(addition(one,multiplication(star(X0),X0)),star(X0))),
  file('/CW/home-0/sutcliff/CASC/23/Problems/FEQ/FEQ073.p',star_unfold_left)).
fof(f10200,plain,(
  ( ! [X0,X1] : (~leq(addition(one,multiplication(X0,X1)),X0) | addition(star(X1),X0) = X0) )),
  inference(resolution,[],[f10100,f34])).
fof(f10100,plain,(
  ( ! [X21,X20] : (leq(star(X20),X21) | ~leq(addition(one,multiplication(X21,X20)),X21)) )),
  inference(forward_demodulation,[],[f10085,f32])).
fof(f10085,plain,(
  ( ! [X21,X20] : (leq(star(X20),X21) | ~leq(addition(multiplication(X21,X20),one),X21)) )),
  inference(superposition,[],[f39,f27])).
fof(f39,plain,(
  ( ! [X2,X0,X1] : (leq(multiplication(X2,star(X1)),X0) | ~leq(addition(multiplication(X0,X1),X2),X0)) )),
  inference(cnf_transformation,[],[f20])).
fof(f20,plain,(
  ! [X0,X1,X2] : (~leq(addition(multiplication(X0,X1),X2),X0) | leq(multiplication(X2,star(X1)),X0))),
  inference(ennf_transformation,[],[f15])).
fof(f15,axiom,(
  ! [X0,X1,X2] : (leq(addition(multiplication(X0,X1),X2),X0) => leq(multiplication(X2,star(X1)),X0))),
  file('/CW/home-0/sutcliff/CASC/23/Problems/FEQ/FEQ073.p',star_induction_right)).
fof(f384136,plain,(
  ( ! [X2] : (addition(star(X2),star(addition(one,X2))) = star(addition(one,X2))) )),
  inference(backward_demodulation,[],[f384089,f172227])).
fof(f172227,plain,(
  ( ! [X2] : (addition(star(addition(X2,one)),star(addition(one,X2))) = star(addition(one,X2))) )),
  inference(superposition,[],[f151735,f1047])).
fof(f1047,plain,(
  ( ! [X118,X117] : (addition(X118,X117) = addition(addition(X117,X118),X117)) )),
  inference(forward_demodulation,[],[f1018,f41])).
fof(f1018,plain,(
  ( ! [X118,X117] : (addition(zero,addition(X118,X117)) = addition(addition(X117,X118),X117)) )),
  inference(superposition,[],[f629,f606])).
fof(f606,plain,(
  ( ! [X2,X3] : (addition(X3,X2) = addition(X2,addition(X2,X3))) )),
  inference(superposition,[],[f146,f226])).
fof(f226,plain,(
  ( ! [X2,X1] : (addition(X2,X1) = addition(X1,addition(X2,X1))) )),
  inference(superposition,[],[f149,f32])).
fof(f629,plain,(
  ( ! [X24,X25] : (addition(X25,X24) = addition(zero,addition(X24,X25))) )),
  inference(superposition,[],[f146,f41])).
fof(f151735,plain,(
  ( ! [X33] : (addition(star(addition(X33,one)),star(X33)) = star(X33)) )),
  inference(subsumption_resolution,[],[f151734,f52])).
fof(f151734,plain,(
  ( ! [X33] : (~leq(star(X33),star(X33)) | addition(star(addition(X33,one)),star(X33)) = star(X33)) )),
  inference(forward_demodulation,[],[f151662,f44367])).
fof(f151662,plain,(
  ( ! [X33] : (~leq(addition(one,star(X33)),star(X33)) | addition(star(addition(X33,one)),star(X33)) = star(X33)) )),
  inference(superposition,[],[f10200,f54602])).
fof(f384089,plain,(
  ( ! [X215] : (star(X215) = star(addition(X215,one))) )),
  inference(forward_demodulation,[],[f383753,f172234])).
fof(f172234,plain,(
  ( ! [X1] : (addition(star(X1),star(addition(X1,one))) = star(X1)) )),
  inference(superposition,[],[f151735,f32])).
fof(f383753,plain,(
  ( ! [X215] : (addition(star(X215),star(addition(X215,one))) = star(addition(X215,one))) )),
  inference(superposition,[],[f44738,f383457])).
fof(f383457,plain,(
  ( ! [X5] : (multiplication(star(addition(X5,one)),star(X5)) = star(addition(X5,one))) )),
  inference(resolution,[],[f68584,f54599])).
fof(f54599,plain,(
  ( ! [X1] : (leq(multiplication(star(X1),X1),star(X1))) )),
  inference(resolution,[],[f46811,f33])).
fof(f68584,plain,(
  ( ! [X0,X1] : (~leq(multiplication(X0,addition(X1,one)),X0) | multiplication(X0,star(X1)) = X0) )),
  inference(forward_demodulation,[],[f68583,f44367])).
fof(f68583,plain,(
  ( ! [X0,X1] : (multiplication(X0,addition(one,star(X1))) = X0 | ~leq(multiplication(X0,addition(X1,one)),X0)) )),
  inference(forward_demodulation,[],[f68582,f2609])).
fof(f2609,plain,(
  ( ! [X0,X1] : (multiplication(X0,addition(one,X1)) = addition(X0,multiplication(X0,X1))) )),
  inference(superposition,[],[f37,f24])).
fof(f68582,plain,(
  ( ! [X0,X1] : (addition(X0,multiplication(X0,star(X1))) = X0 | ~leq(multiplication(X0,addition(X1,one)),X0)) )),
  inference(forward_demodulation,[],[f68504,f32])).
fof(f68504,plain,(
  ( ! [X0,X1] : (~leq(multiplication(X0,addition(X1,one)),X0) | addition(multiplication(X0,star(X1)),X0) = X0) )),
  inference(superposition,[],[f10076,f2614])).
fof(f10076,plain,(
  ( ! [X2,X0,X1] : (~leq(addition(multiplication(X0,X1),X2),X0) | addition(multiplication(X2,star(X1)),X0) = X0) )),
  inference(resolution,[],[f39,f34])).
fof(f44738,plain,(
  ( ! [X0,X1] : (multiplication(star(X1),X0) = addition(X0,multiplication(star(X1),X0))) )),
  inference(resolution,[],[f44318,f34])).
fof(f44318,plain,(
  ( ! [X80,X81] : (leq(X81,multiplication(star(X80),X81))) )),
  inference(superposition,[],[f7024,f44186])).
fof(f7024,plain,(
  ( ! [X17,X16] : (leq(X16,multiplication(addition(one,X17),X16))) )),
  inference(superposition,[],[f6857,f27])).
fof(f6857,plain,(
  ( ! [X57,X58,X56] : (leq(multiplication(X56,X57),multiplication(addition(X56,X58),X57))) )),
  inference(superposition,[],[f224,f38])).
fof(f224,plain,(
  ( ! [X0,X1] : (leq(X0,addition(X0,X1))) )),
  inference(resolution,[],[f149,f33])).
fof(f418628,plain,(
  ~leq(star(one),one)),
  inference(backtracking_split_refutation,[],[f174,f179_D,f418560])).
fof(f418560,plain,(
  $false | $spl2),
  inference(resolution,[],[f416114,f23])).
fof(f23,plain,(
  ~leq(multiplication(a,multiplication(a,multiplication(a,a))),star(a))),
  inference(cnf_transformation,[],[f19])).
fof(f19,plain,(
  ~leq(multiplication(a,multiplication(a,multiplication(a,a))),star(a))),
  inference(ennf_transformation,[],[f17])).
fof(f17,negated_conjecture,(
  ~leq(multiplication(a,multiplication(a,multiplication(a,a))),star(a))),
  file('/CW/home-0/sutcliff/CASC/23/Problems/FEQ/FEQ073.p',a)).
fof(f416114,plain,(
  ( ! [X271] : (leq(multiplication(X271,multiplication(X271,multiplication(X271,X271))),star(X271))) ) | $spl2),
  inference(forward_demodulation,[],[f415034,f36])).
fof(f36,plain,(
  ( ! [X2,X0,X1] : (multiplication(multiplication(X0,X1),X2) = multiplication(X0,multiplication(X1,X2))) )),
  inference(cnf_transformation,[],[f14])).
fof(f14,axiom,(
  ! [X0,X1,X2] : multiplication(multiplication(X0,X1),X2) = multiplication(X0,multiplication(X1,X2))),
  file('/CW/home-0/sutcliff/CASC/23/Problems/FEQ/FEQ073.p',multiplicative_associativity)).
fof(f415034,plain,(
  ( ! [X271] : (leq(multiplication(multiplication(X271,X271),multiplication(X271,X271)),star(X271))) ) | $spl2),
  inference(superposition,[],[f72259,f412366])).
fof(f412366,plain,(
  ( ! [X0] : (addition(star(X0),star(multiplication(X0,X0))) = star(X0)) ) | $spl2),
  inference(resolution,[],[f390070,f18008])).
fof(f18008,plain,(
  ( ! [X4,X3] : (~leq(addition(X3,X4),X3) | addition(X3,X4) = X3) ) | $spl2),
  inference(resolution,[],[f13906,f10122])).
fof(f10122,plain,(
  ( ! [X19,X18] : (leq(addition(X19,X18),X18) | ~leq(addition(X18,X19),X18)) ) | $spl2),
  inference(superposition,[],[f10105,f613])).
fof(f613,plain,(
  ( ! [X0,X1] : (addition(X0,X1) = addition(X0,addition(X1,X0))) )),
  inference(superposition,[],[f146,f149])).
fof(f10105,plain,(
  ( ! [X2,X3] : (~leq(addition(X3,X2),X3) | leq(X2,X3)) ) | $spl2),
  inference(forward_demodulation,[],[f10104,f24])).
fof(f10104,plain,(
  ( ! [X2,X3] : (leq(X2,X3) | ~leq(addition(multiplication(X3,one),X2),X3)) ) | $spl2),
  inference(forward_demodulation,[],[f10087,f24])).
fof(f10087,plain,(
  ( ! [X2,X3] : (leq(multiplication(X2,one),X3) | ~leq(addition(multiplication(X3,one),X2),X3)) ) | $spl2),
  inference(superposition,[],[f39,f190])).
fof(f190,plain,(
  one = star(one) | $spl2),
  inference(backward_demodulation,[],[f182,f163])).
fof(f163,plain,(
  addition(one,star(one)) = star(one)),
  inference(forward_demodulation,[],[f143,f26])).
fof(f143,plain,(
  addition(one,addition(star(one),star(one))) = star(one)),
  inference(superposition,[],[f35,f94])).
fof(f94,plain,(
  addition(addition(one,star(one)),star(one)) = star(one)),
  inference(resolution,[],[f90,f34])).
fof(f90,plain,(
  leq(addition(one,star(one)),star(one))),
  inference(superposition,[],[f30,f27])).
fof(f182,plain,(
  addition(one,star(one)) = one | $spl2),
  inference(superposition,[],[f180,f32])).
fof(f180,plain,(
  addition(star(one),one) = one | $spl2),
  inference(resolution,[],[f179,f34])).
fof(f13906,plain,(
  ( ! [X4,X3] : (~leq(addition(X3,X4),X4) | addition(X4,X3) = X4) ) | $spl2),
  inference(forward_demodulation,[],[f13905,f149])).
fof(f13905,plain,(
  ( ! [X4,X3] : (addition(X4,addition(X4,X3)) = X4 | ~leq(addition(X3,X4),X4)) ) | $spl2),
  inference(forward_demodulation,[],[f13864,f32])).
fof(f13864,plain,(
  ( ! [X4,X3] : (~leq(addition(X3,X4),X4) | addition(addition(X4,X3),X4) = X4) ) | $spl2),
  inference(resolution,[],[f10120,f34])).
fof(f10120,plain,(
  ( ! [X14,X15] : (leq(addition(X14,X15),X14) | ~leq(addition(X15,X14),X14)) ) | $spl2),
  inference(superposition,[],[f10105,f606])).
fof(f390070,plain,(
  ( ! [X192] : (leq(addition(star(X192),star(multiplication(X192,X192))),star(X192))) ) | $spl2),
  inference(forward_demodulation,[],[f389895,f103984])).
fof(f103984,plain,(
  ( ! [X1] : (star(X1) = star(star(X1))) ) | $spl2),
  inference(superposition,[],[f103372,f46904])).
fof(f46904,plain,(
  ( ! [X0] : (addition(star(X0),X0) = star(X0)) ) | $spl2),
  inference(resolution,[],[f46590,f18010])).
fof(f18010,plain,(
  ( ! [X8,X7] : (addition(X8,X7) != X7 | addition(X7,X8) = X7) ) | $spl2),
  inference(resolution,[],[f13906,f305])).
fof(f305,plain,(
  ( ! [X14,X15] : (leq(addition(X15,X14),X14) | addition(X15,X14) != X14) )),
  inference(superposition,[],[f56,f226])).
fof(f56,plain,(
  ( ! [X2,X3] : (addition(X3,X2) != X3 | leq(X2,X3)) )),
  inference(superposition,[],[f33,f32])).
fof(f46590,plain,(
  ( ! [X0] : (addition(X0,star(X0)) = star(X0)) )),
  inference(resolution,[],[f46325,f34])).
fof(f46325,plain,(
  ( ! [X1] : (leq(X1,star(X1))) )),
  inference(superposition,[],[f44302,f44567])).
fof(f44567,plain,(
  ( ! [X3] : (addition(multiplication(X3,star(X3)),star(X3)) = star(X3)) )),
  inference(backward_demodulation,[],[f44367,f44188])).
fof(f44188,plain,(
  ( ! [X3] : (addition(multiplication(X3,star(X3)),addition(one,star(X3))) = star(X3)) )),
  inference(forward_demodulation,[],[f43986,f32])).
fof(f43986,plain,(
  ( ! [X3] : (addition(multiplication(X3,star(X3)),addition(star(X3),one)) = star(X3)) )),
  inference(superposition,[],[f89,f609])).
fof(f44302,plain,(
  ( ! [X26,X27,X25] : (leq(X26,addition(multiplication(X26,star(X25)),X27))) )),
  inference(superposition,[],[f3011,f44186])).
fof(f3011,plain,(
  ( ! [X6,X4,X5] : (leq(X5,addition(multiplication(X5,addition(one,X6)),X4))) )),
  inference(superposition,[],[f2926,f32])).
fof(f2926,plain,(
  ( ! [X39,X41,X40] : (leq(X39,addition(X41,multiplication(X39,addition(one,X40))))) )),
  inference(superposition,[],[f260,f2609])).
fof(f260,plain,(
  ( ! [X4,X2,X3] : (leq(X3,addition(X4,addition(X3,X2)))) )),
  inference(superposition,[],[f257,f32])).
fof(f257,plain,(
  ( ! [X10,X11,X9] : (leq(X11,addition(X9,addition(X10,X11)))) )),
  inference(superposition,[],[f244,f35])).
fof(f244,plain,(
  ( ! [X2,X1] : (leq(X1,addition(X2,X1))) )),
  inference(superposition,[],[f224,f32])).
fof(f103372,plain,(
  ( ! [X29] : (addition(star(star(X29)),star(X29)) = star(X29)) )),
  inference(forward_demodulation,[],[f103371,f55452])).
fof(f55452,plain,(
  ( ! [X18] : (multiplication(star(star(X18)),star(X18)) = star(star(X18))) )),
  inference(superposition,[],[f54602,f44427])).
fof(f44427,plain,(
  ( ! [X325] : (addition(star(X325),one) = star(X325)) )),
  inference(superposition,[],[f922,f44186])).
fof(f922,plain,(
  ( ! [X6,X7] : (addition(X6,X7) = addition(addition(X6,X7),X6)) )),
  inference(forward_demodulation,[],[f867,f41])).
fof(f867,plain,(
  ( ! [X6,X7] : (addition(zero,addition(X6,X7)) = addition(addition(X6,X7),X6)) )),
  inference(superposition,[],[f629,f149])).
fof(f103371,plain,(
  ( ! [X29] : (addition(multiplication(star(star(X29)),star(X29)),star(X29)) = star(X29)) )),
  inference(subsumption_resolution,[],[f102886,f52])).
fof(f102886,plain,(
  ( ! [X29] : (~leq(star(X29),star(X29)) | addition(multiplication(star(star(X29)),star(X29)),star(X29)) = star(X29)) )),
  inference(superposition,[],[f15218,f68596])).
fof(f68596,plain,(
  ( ! [X17] : (addition(multiplication(star(X17),star(X17)),star(X17)) = star(X17)) )),
  inference(subsumption_resolution,[],[f68511,f52])).
fof(f68511,plain,(
  ( ! [X17] : (~leq(star(X17),star(X17)) | addition(multiplication(star(X17),star(X17)),star(X17)) = star(X17)) )),
  inference(superposition,[],[f10076,f46811])).
fof(f15218,plain,(
  ( ! [X2,X0,X1] : (~leq(addition(multiplication(X0,X1),X2),X1) | addition(multiplication(star(X0),X2),X1) = X1) )),
  inference(resolution,[],[f40,f34])).
fof(f389895,plain,(
  ( ! [X192] : (leq(addition(star(X192),star(multiplication(X192,X192))),star(star(X192)))) ) | $spl2),
  inference(superposition,[],[f386847,f72128])).
fof(f72128,plain,(
  ( ! [X0] : (addition(star(X0),multiplication(X0,X0)) = star(X0)) ) | $spl2),
  inference(resolution,[],[f72117,f18010])).
fof(f72117,plain,(
  ( ! [X0] : (addition(multiplication(X0,X0),star(X0)) = star(X0)) )),
  inference(resolution,[],[f72054,f34])).
fof(f72054,plain,(
  ( ! [X0] : (leq(multiplication(X0,X0),star(X0))) )),
  inference(superposition,[],[f47073,f44567])).
fof(f47073,plain,(
  ( ! [X346,X345,X347] : (leq(multiplication(X346,X345),addition(multiplication(X346,star(X345)),X347))) )),
  inference(superposition,[],[f15060,f46590])).
fof(f15060,plain,(
  ( ! [X17,X15,X18,X16] : (leq(multiplication(X16,X17),addition(multiplication(X16,addition(X17,X18)),X15))) )),
  inference(superposition,[],[f2636,f32])).
fof(f2636,plain,(
  ( ! [X59,X57,X60,X58] : (leq(multiplication(X57,X58),addition(X60,multiplication(X57,addition(X58,X59))))) )),
  inference(superposition,[],[f260,f37])).
fof(f386847,plain,(
  ( ! [X12,X13] : (leq(addition(X13,star(X12)),star(addition(X13,X12)))) )),
  inference(backward_demodulation,[],[f386811,f302837])).
fof(f302837,plain,(
  ( ! [X12,X13] : (leq(addition(X13,star(X12)),multiplication(star(addition(X13,X12)),star(X12)))) )),
  inference(superposition,[],[f302700,f46922])).
fof(f46922,plain,(
  ( ! [X17,X18] : (addition(X18,star(X17)) = addition(star(X17),addition(X18,X17))) )),
  inference(superposition,[],[f146,f46590])).
fof(f302700,plain,(
  ( ! [X0,X1] : (leq(addition(star(X0),X1),multiplication(star(X1),star(X0)))) )),
  inference(superposition,[],[f108878,f44738])).
fof(f108878,plain,(
  ( ! [X1725,X1724,X1723] : (leq(addition(X1725,X1723),addition(X1725,multiplication(star(X1723),star(X1724))))) )),
  inference(superposition,[],[f70321,f44724])).
fof(f44724,plain,(
  ( ! [X0,X1] : (multiplication(X0,star(X1)) = addition(X0,multiplication(X0,star(X1)))) )),
  inference(resolution,[],[f44294,f34])).
fof(f44294,plain,(
  ( ! [X0,X1] : (leq(X1,multiplication(X1,star(X0)))) )),
  inference(superposition,[],[f2726,f44186])).
fof(f2726,plain,(
  ( ! [X0,X1] : (leq(X0,multiplication(X0,addition(one,X1)))) )),
  inference(superposition,[],[f2629,f24])).
fof(f2629,plain,(
  ( ! [X35,X33,X34] : (leq(multiplication(X33,X34),multiplication(X33,addition(X34,X35)))) )),
  inference(superposition,[],[f224,f37])).
fof(f70321,plain,(
  ( ! [X10,X8,X9] : (leq(addition(X9,X10),addition(X9,addition(star(X10),X8)))) )),
  inference(superposition,[],[f46936,f146])).
fof(f46936,plain,(
  ( ! [X45,X43,X44] : (leq(addition(X44,X43),addition(X45,addition(X44,star(X43))))) )),
  inference(superposition,[],[f287,f46590])).
fof(f287,plain,(
  ( ! [X17,X15,X18,X16] : (leq(addition(X15,X16),addition(X18,addition(X15,addition(X16,X17))))) )),
  inference(superposition,[],[f260,f35])).
fof(f386811,plain,(
  ( ! [X8,X9] : (multiplication(star(addition(X9,X8)),star(X8)) = star(addition(X9,X8))) )),
  inference(backward_demodulation,[],[f386748,f383509])).
fof(f383509,plain,(
  ( ! [X8,X9] : (multiplication(star(addition(X8,addition(one,X9))),star(X8)) = star(addition(X8,addition(one,X9)))) )),
  inference(forward_demodulation,[],[f383459,f35])).
fof(f383459,plain,(
  ( ! [X8,X9] : (multiplication(star(addition(addition(X8,one),X9)),star(X8)) = star(addition(addition(X8,one),X9))) )),
  inference(resolution,[],[f68584,f54618])).
fof(f54618,plain,(
  ( ! [X14,X13] : (leq(multiplication(star(addition(X13,X14)),X13),star(addition(X13,X14)))) )),
  inference(superposition,[],[f15060,f46811])).
fof(f386748,plain,(
  ( ! [X19,X20] : (star(addition(X19,X20)) = star(addition(X20,addition(one,X19)))) )),
  inference(forward_demodulation,[],[f385379,f384457])).
fof(f385379,plain,(
  ( ! [X19,X20] : (star(addition(one,addition(X19,X20))) = star(addition(X20,addition(one,X19)))) )),
  inference(superposition,[],[f384457,f729])).
fof(f729,plain,(
  ( ! [X12,X10,X11] : (addition(X12,addition(X10,X11)) = addition(X10,addition(X10,addition(X11,X12)))) )),
  inference(forward_demodulation,[],[f625,f35])).
fof(f625,plain,(
  ( ! [X12,X10,X11] : (addition(X12,addition(X10,X11)) = addition(X10,addition(addition(X10,X11),X12))) )),
  inference(superposition,[],[f146,f149])).
fof(f72259,plain,(
  ( ! [X196,X197] : (leq(multiplication(X196,X196),addition(X197,star(X196)))) )),
  inference(superposition,[],[f260,f72117])).
fof(f179,plain,(
  leq(star(one),one) | $spl2),
  inference(cnf_transformation,[],[f179_D])).
fof(f179_D,plain,(
  leq(star(one),one) <=> ~$spl2),
  introduced(backtracking_splitting_component,[])).
fof(f174,plain,(
  one != star(one) | leq(star(one),one)),
  inference(superposition,[],[f56,f163])).
% SZS output end Proof for FEQ073
------------------------------
Version: Vampire 1.0 (revision 700)
Termination reason: Refutation

Active clauses: 2782
Passive clauses: 42682
Generated clauses: 463568
Final active clauses: 1129
Final passive clauses: 17354
Input formulas: 17
Initial clauses: 18

Trivial inequalities: 324
Fw subsumption resolutions: 263
Fw demodulations: 135022
Bw demodulations: 17887

Simple tautologies: 485
Equational tautologies: 6
Forward subsumptions: 283582
Backward subsumptions: 1795
Fw demodulations to eq. taut.: 1178
Bw demodulations to eq. taut.: 8

Binary resolution: 3516
Forward superposition: 176666
Backward superposition: 97023
Self superposition: 175
Equality resolution: 15

Backtracking splits: 4
Backtracking splits refuted: 4
Backtracking splits refuted at zero level: 2

Memory used: 199570KB
Time elapsed: 10.548 s
------------------------------
% Success in time 90.46 s

WATCH: 90.38 CPU 90.48 WC

FINAL WATCH: 90.38 CPU 90.48 WC