%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GRP664-12 : TPTP v9.3.1. Released v8.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n014.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 10:15:30 AM UTC 2026
% Result : Unsatisfiable 89.87s 23.75s
% Output : Refutation 163.51s
% Verified :
% SZS Type : Refutation
% Derivation depth : 79
% Number of leaves : 10
% Syntax : Number of formulae : 329 ( 329 unt; 0 def)
% Number of atoms : 329 ( 328 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 2 ( 2 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 2 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 8 ( 8 usr; 5 con; 0-2 aty)
% Number of variables : 477 ( 477 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] : mult(X0,ld(X0,X1)) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',f01) ).
fof(f2,axiom,
! [X0,X1] : ld(X0,mult(X0,X1)) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',f02) ).
fof(f3,axiom,
! [X0,X1] : mult(rd(X0,X1),X1) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',f03) ).
fof(f4,axiom,
! [X0,X1] : rd(mult(X0,X1),X1) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',f04) ).
fof(f5,axiom,
! [X0] : mult(X0,unit) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',f05) ).
fof(f6,axiom,
! [X0] : mult(unit,X0) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',f06) ).
fof(f7,axiom,
! [X2,X0,X1] : mult(X0,mult(X1,X2)) = mult(rd(mult(X0,X1),X0),mult(X0,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',f07) ).
fof(f8,axiom,
! [X2,X0,X1] : mult(mult(X0,X1),X2) = mult(mult(X0,X2),ld(X2,mult(X1,X2))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',f08) ).
fof(f9,negated_conjecture,
mult(x0,x1) = unit,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goal1) ).
fof(f10,plain,
unit = mult(x0,x1),
inference(reorient_equations,[],[f9]) ).
fof(f11,negated_conjecture,
mult(mult(x2,x3),mult(x1,x0)) != mult(x2,mult(x3,mult(x1,x0))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goal2) ).
fof(f18,plain,
! [X2,X3,X0,X1] : mult(mult(X3,rd(mult(X0,X1),X0)),mult(X0,X2)) = mult(mult(X3,mult(X0,X2)),ld(mult(X0,X2),mult(X0,mult(X1,X2)))),
inference(superposition,[],[f8,f7]) ).
fof(f19,plain,
! [X2,X3,X0,X1] : mult(mult(rd(mult(X0,X1),X0),X3),mult(X0,X2)) = mult(mult(X0,mult(X1,X2)),ld(mult(X0,X2),mult(X3,mult(X0,X2)))),
inference(superposition,[],[f8,f7]) ).
fof(f20,plain,
! [X0] : mult(x0,mult(X0,x1)) = mult(rd(mult(x0,X0),x0),unit),
inference(superposition,[],[f7,f10]) ).
fof(f22,plain,
! [X0] : mult(mult(X0,x0),x1) = mult(mult(X0,x1),ld(x1,unit)),
inference(superposition,[],[f8,f10]) ).
fof(f23,plain,
! [X0] : mult(mult(x0,X0),x1) = mult(unit,ld(x1,mult(X0,x1))),
inference(superposition,[],[f8,f10]) ).
fof(f24,plain,
! [X0] : mult(mult(x0,X0),x1) = ld(x1,mult(X0,x1)),
inference(forward_demodulation,[],[f23,f6]) ).
fof(f25,plain,
! [X0] : mult(x0,mult(X0,x1)) = rd(mult(x0,X0),x0),
inference(forward_demodulation,[],[f20,f5]) ).
fof(f47,plain,
! [X2,X0,X1] : mult(X1,mult(X2,ld(X1,X0))) = mult(rd(mult(X1,X2),X1),X0),
inference(superposition,[],[f7,f1]) ).
fof(f48,plain,
! [X2,X0,X1] : mult(X1,mult(ld(X1,X0),X2)) = mult(rd(X0,X1),mult(X1,X2)),
inference(superposition,[],[f7,f1]) ).
fof(f49,plain,
! [X2,X0,X1] : mult(mult(X1,X2),ld(X2,X0)) = mult(mult(X1,ld(X2,X0)),ld(ld(X2,X0),X0)),
inference(superposition,[],[f8,f1]) ).
fof(f51,plain,
! [X0] : ld(unit,X0) = X0,
inference(superposition,[],[f6,f1]) ).
fof(f58,plain,
! [X2,X3,X0,X1] : mult(mult(X0,mult(X1,X2)),ld(mult(X0,X2),mult(X3,mult(X0,X2)))) = mult(mult(X0,mult(X1,ld(X0,X3))),mult(X0,X2)),
inference(backward_demodulation,[],[f19,f47]) ).
fof(f63,plain,
! [X0] : unit = ld(X0,X0),
inference(superposition,[],[f2,f5]) ).
fof(f64,plain,
! [X2,X0,X1] : ld(X2,mult(X1,X2)) = ld(mult(X0,X2),mult(mult(X0,X1),X2)),
inference(superposition,[],[f2,f8]) ).
fof(f66,plain,
x1 = ld(x0,unit),
inference(superposition,[],[f2,f10]) ).
fof(f70,plain,
! [X0,X1] : ld(rd(X0,X1),X0) = X1,
inference(superposition,[],[f2,f3]) ).
fof(f71,plain,
! [X2,X0,X1] : mult(mult(X1,X2),ld(X2,X0)) = mult(mult(X1,rd(X0,X2)),X2),
inference(superposition,[],[f8,f3]) ).
fof(f72,plain,
! [X2,X0,X1] : mult(X0,ld(X1,mult(X2,X1))) = mult(mult(rd(X0,X1),X2),X1),
inference(superposition,[],[f8,f3]) ).
fof(f73,plain,
! [X0] : rd(X0,unit) = X0,
inference(superposition,[],[f5,f3]) ).
fof(f75,plain,
! [X0,X1] : rd(X0,ld(X1,X0)) = X1,
inference(superposition,[],[f4,f1]) ).
fof(f76,plain,
! [X2,X0,X1] : mult(X0,X2) = rd(mult(mult(X0,X1),X2),ld(X2,mult(X1,X2))),
inference(superposition,[],[f4,f8]) ).
fof(f77,plain,
! [X0] : unit = rd(X0,X0),
inference(superposition,[],[f4,f6]) ).
fof(f80,plain,
! [X2,X0,X1] : ld(ld(X1,X0),mult(X2,ld(X1,X0))) = ld(X0,mult(mult(X1,X2),ld(X1,X0))),
inference(superposition,[],[f64,f1]) ).
fof(f86,plain,
! [X2,X0,X1] : ld(X1,mult(ld(X2,X0),X1)) = ld(mult(X2,X1),mult(X0,X1)),
inference(superposition,[],[f64,f1]) ).
fof(f130,plain,
mult(mult(x0,x0),x1) = mult(unit,ld(x1,unit)),
inference(superposition,[],[f22,f10]) ).
fof(f137,plain,
ld(x1,unit) = mult(mult(x0,x0),x1),
inference(forward_demodulation,[],[f130,f6]) ).
fof(f145,plain,
rd(unit,x0) = mult(x0,mult(x1,x1)),
inference(superposition,[],[f25,f10]) ).
fof(f147,plain,
! [X0] : mult(x0,mult(ld(x0,X0),x1)) = rd(X0,x0),
inference(superposition,[],[f25,f1]) ).
fof(f161,plain,
! [X2,X0,X1] : mult(X0,rd(X2,X1)) = rd(mult(mult(X0,X1),ld(X1,X2)),X1),
inference(superposition,[],[f4,f71]) ).
fof(f174,plain,
! [X2,X0,X1] : mult(X0,mult(X1,X2)) = mult(X1,mult(ld(X1,mult(X0,X1)),X2)),
inference(superposition,[],[f48,f4]) ).
fof(f175,plain,
! [X0,X1] : mult(x0,mult(ld(x0,mult(x0,X0)),X1)) = mult(mult(x0,mult(X0,x1)),mult(x0,X1)),
inference(superposition,[],[f48,f25]) ).
fof(f177,plain,
! [X2,X0,X1] : mult(X1,mult(ld(X1,X2),ld(X1,X0))) = mult(rd(X2,X1),X0),
inference(superposition,[],[f48,f1]) ).
fof(f194,plain,
! [X0,X1] : mult(mult(x0,mult(X0,x1)),mult(x0,X1)) = mult(x0,mult(X0,X1)),
inference(forward_demodulation,[],[f175,f2]) ).
fof(f254,plain,
! [X2,X0,X1] : mult(rd(X0,X1),X2) = rd(mult(X0,X2),ld(X2,mult(X1,X2))),
inference(superposition,[],[f76,f3]) ).
fof(f334,plain,
! [X0,X1] : mult(x0,mult(rd(X0,x1),X1)) = mult(mult(x0,X0),mult(x0,X1)),
inference(superposition,[],[f194,f3]) ).
fof(f392,plain,
! [X0] : mult(x0,mult(x1,X0)) = mult(x1,mult(ld(x1,unit),X0)),
inference(superposition,[],[f174,f10]) ).
fof(f394,plain,
! [X2,X0,X1] : mult(X2,X0) = mult(X1,mult(X2,ld(ld(X2,mult(X1,X2)),X0))),
inference(superposition,[],[f174,f1]) ).
fof(f397,plain,
! [X2,X0,X1] : mult(ld(X1,mult(X0,X1)),X2) = ld(X1,mult(X0,mult(X1,X2))),
inference(superposition,[],[f2,f174]) ).
fof(f432,plain,
! [X0] : mult(x0,mult(x1,ld(x0,X0))) = mult(rd(unit,x0),X0),
inference(superposition,[],[f47,f10]) ).
fof(f445,plain,
! [X2,X0,X1] : rd(mult(X0,X1),X0) = rd(mult(X0,mult(X1,ld(X0,X2))),X2),
inference(superposition,[],[f4,f47]) ).
fof(f453,plain,
! [X0,X1] : rd(mult(X0,X1),X0) = mult(X0,mult(X1,ld(X0,unit))),
inference(superposition,[],[f5,f47]) ).
fof(f489,plain,
! [X0,X1] : mult(X0,mult(x1,X1)) = mult(x1,mult(mult(mult(x0,X0),x1),X1)),
inference(superposition,[],[f174,f24]) ).
fof(f490,plain,
! [X0,X1] : mult(mult(X1,X0),x1) = mult(mult(X1,x1),mult(mult(x0,X0),x1)),
inference(superposition,[],[f8,f24]) ).
fof(f494,plain,
! [X0] : mult(X0,x1) = mult(x1,mult(mult(x0,X0),x1)),
inference(superposition,[],[f1,f24]) ).
fof(f513,plain,
! [X0,X1] : mult(mult(X1,ld(x0,X0)),x1) = mult(mult(X1,x1),mult(X0,x1)),
inference(superposition,[],[f490,f1]) ).
fof(f554,plain,
! [X0] : mult(ld(x0,X0),x1) = mult(x1,mult(X0,x1)),
inference(superposition,[],[f494,f1]) ).
fof(f573,plain,
! [X0] : rd(X0,x0) = mult(x0,mult(x1,mult(X0,x1))),
inference(backward_demodulation,[],[f147,f554]) ).
fof(f594,plain,
! [X0] : mult(x0,mult(x1,X0)) = rd(rd(X0,x1),x0),
inference(superposition,[],[f573,f3]) ).
fof(f604,plain,
! [X0] : mult(x1,mult(X0,x1)) = ld(x0,rd(X0,x0)),
inference(superposition,[],[f2,f573]) ).
fof(f630,plain,
! [X0,X1] : mult(ld(x0,X0),mult(x1,X1)) = mult(x1,mult(ld(x1,mult(x1,mult(X0,x1))),X1)),
inference(superposition,[],[f174,f554]) ).
fof(f631,plain,
! [X0,X1] : mult(ld(x0,X0),mult(x1,X1)) = mult(x1,mult(mult(X0,x1),X1)),
inference(forward_demodulation,[],[f630,f2]) ).
fof(f655,plain,
! [X0,X1] : mult(X0,x1) = mult(mult(rd(X0,ld(x0,X1)),x1),mult(X1,x1)),
inference(superposition,[],[f513,f3]) ).
fof(f667,plain,
! [X0,X1] : mult(X0,ld(x0,X1)) = rd(mult(mult(X0,x1),mult(X1,x1)),x1),
inference(superposition,[],[f4,f513]) ).
fof(f704,plain,
! [X2,X0,X1] : rd(X0,ld(X1,mult(X2,X1))) = mult(rd(rd(X0,X1),X2),X1),
inference(superposition,[],[f254,f3]) ).
fof(f722,plain,
! [X2,X0,X1] : mult(rd(X1,rd(X0,X2)),X2) = rd(mult(X1,X2),ld(X2,X0)),
inference(superposition,[],[f254,f3]) ).
fof(f877,plain,
! [X2,X0,X1] : ld(X1,mult(ld(X2,rd(X0,X1)),X1)) = ld(mult(X2,X1),X0),
inference(superposition,[],[f86,f3]) ).
fof(f983,plain,
! [X0] : ld(x0,X0) = mult(x1,mult(mult(X0,x0),x1)),
inference(superposition,[],[f604,f4]) ).
fof(f1001,plain,
! [X0] : ld(x0,rd(X0,x1)) = mult(x1,mult(X0,ld(x1,mult(x0,x1)))),
inference(superposition,[],[f983,f72]) ).
fof(f1005,plain,
! [X0] : mult(mult(X0,x0),x1) = ld(x1,ld(x0,X0)),
inference(superposition,[],[f2,f983]) ).
fof(f1017,plain,
! [X0] : ld(x0,rd(X0,x1)) = mult(x1,mult(X0,mult(mult(x0,x0),x1))),
inference(forward_demodulation,[],[f1001,f24]) ).
fof(f1022,plain,
! [X0] : ld(x0,rd(X0,x1)) = mult(x1,mult(X0,ld(x1,unit))),
inference(forward_demodulation,[],[f1017,f137]) ).
fof(f1024,plain,
! [X0] : ld(x0,rd(X0,x1)) = rd(mult(x1,X0),x1),
inference(forward_demodulation,[],[f1022,f453]) ).
fof(f1041,plain,
! [X2,X0,X1] : rd(mult(X1,X2),X1) = rd(mult(X1,mult(X2,X0)),mult(X1,X0)),
inference(superposition,[],[f445,f2]) ).
fof(f1113,plain,
! [X2,X0,X1] : rd(mult(X1,X2),X1) = rd(mult(X1,X0),mult(X1,ld(X2,X0))),
inference(superposition,[],[f1041,f1]) ).
fof(f1123,plain,
! [X2,X0,X1] : rd(mult(X1,rd(X0,X2)),X1) = rd(mult(X1,X0),mult(X1,X2)),
inference(superposition,[],[f1041,f3]) ).
fof(f1127,plain,
! [X0] : rd(mult(X0,x0),X0) = rd(mult(X0,unit),mult(X0,x1)),
inference(superposition,[],[f1041,f10]) ).
fof(f1191,plain,
! [X0] : rd(mult(X0,x0),X0) = rd(X0,mult(X0,x1)),
inference(forward_demodulation,[],[f1127,f5]) ).
fof(f1251,plain,
! [X0,X1] : rd(mult(X0,X1),X0) = rd(X0,mult(X0,ld(X1,unit))),
inference(superposition,[],[f1113,f5]) ).
fof(f1262,plain,
! [X2,X0,X1] : rd(mult(rd(X0,X1),X2),rd(X0,X1)) = rd(X0,mult(rd(X0,X1),ld(X2,X1))),
inference(superposition,[],[f1113,f3]) ).
fof(f1539,plain,
! [X0,X1] : mult(rd(X0,x1),ld(x0,X1)) = rd(mult(X0,mult(X1,x1)),x1),
inference(superposition,[],[f667,f3]) ).
fof(f1618,plain,
! [X0,X1] : rd(mult(x1,X0),mult(x1,X1)) = ld(x0,rd(rd(X0,X1),x1)),
inference(superposition,[],[f1123,f1024]) ).
fof(f1691,plain,
! [X2,X0,X1] : ld(X1,mult(X2,X0)) = mult(ld(X1,mult(X2,X1)),ld(X1,X0)),
inference(superposition,[],[f397,f1]) ).
fof(f1715,plain,
! [X2,X0,X1] : ld(X1,X0) = mult(ld(X1,mult(rd(X0,mult(X1,X2)),X1)),X2),
inference(superposition,[],[f397,f3]) ).
fof(f1809,plain,
! [X0,X1] : mult(mult(ld(x0,mult(X0,x0)),x1),mult(X1,x1)) = mult(ld(x0,mult(X0,X1)),x1),
inference(superposition,[],[f513,f1691]) ).
fof(f1815,plain,
! [X2,X0,X1] : ld(X0,mult(X1,X0)) = rd(ld(X0,mult(X1,X2)),ld(X0,X2)),
inference(superposition,[],[f4,f1691]) ).
fof(f1839,plain,
! [X0,X1] : mult(mult(ld(x0,mult(X0,x0)),x1),mult(X1,x1)) = mult(x1,mult(mult(X0,X1),x1)),
inference(forward_demodulation,[],[f1809,f554]) ).
fof(f1863,plain,
! [X0,X1] : mult(x1,mult(mult(X0,X1),x1)) = mult(mult(x1,mult(mult(X0,x0),x1)),mult(X1,x1)),
inference(forward_demodulation,[],[f1839,f554]) ).
fof(f1878,plain,
! [X0,X1] : mult(ld(x0,X0),mult(X1,x1)) = mult(x1,mult(mult(X0,X1),x1)),
inference(forward_demodulation,[],[f1863,f983]) ).
fof(f1887,plain,
! [X0,X1] : mult(X0,mult(X1,x1)) = mult(x1,mult(mult(mult(x0,X0),X1),x1)),
inference(superposition,[],[f1878,f2]) ).
fof(f1957,plain,
! [X0,X1] : mult(x1,mult(X0,x1)) = mult(X1,mult(ld(mult(x0,X1),X0),x1)),
inference(superposition,[],[f1887,f1]) ).
fof(f1964,plain,
! [X0,X1] : rd(mult(X0,mult(X1,x1)),x1) = ld(x0,rd(mult(mult(mult(x0,X0),X1),x1),x1)),
inference(superposition,[],[f1024,f1887]) ).
fof(f1986,plain,
! [X0,X1] : rd(mult(X0,mult(X1,x1)),x1) = ld(x0,mult(mult(x0,X0),X1)),
inference(forward_demodulation,[],[f1964,f4]) ).
fof(f1998,plain,
! [X0,X1] : mult(rd(X0,x1),ld(x0,X1)) = ld(x0,mult(mult(x0,X0),X1)),
inference(forward_demodulation,[],[f1986,f1539]) ).
fof(f2019,plain,
! [X0,X1] : rd(mult(X1,ld(mult(x0,X1),X0)),X1) = rd(mult(x1,mult(X0,x1)),mult(X1,x1)),
inference(superposition,[],[f1041,f1957]) ).
fof(f2020,plain,
! [X0,X1] : ld(X1,mult(x1,mult(X0,x1))) = mult(ld(mult(x0,X1),X0),x1),
inference(superposition,[],[f2,f1957]) ).
fof(f2180,plain,
! [X2,X0,X1] : mult(rd(X0,X1),rd(X2,X1)) = rd(mult(X0,ld(X1,X2)),X1),
inference(superposition,[],[f161,f3]) ).
fof(f2184,plain,
! [X0] : mult(x0,rd(X0,x1)) = rd(mult(unit,ld(x1,X0)),x1),
inference(superposition,[],[f161,f10]) ).
fof(f2195,plain,
! [X2,X0,X1] : mult(X1,rd(mult(X2,X0),X2)) = rd(mult(mult(X1,X2),X0),X2),
inference(superposition,[],[f161,f2]) ).
fof(f2236,plain,
! [X0] : mult(x0,rd(X0,x1)) = rd(ld(x1,X0),x1),
inference(forward_demodulation,[],[f2184,f6]) ).
fof(f2336,plain,
! [X0,X1] : mult(mult(x0,X1),X0) = mult(x0,mult(rd(X1,x1),ld(x0,X0))),
inference(superposition,[],[f334,f1]) ).
fof(f2886,plain,
! [X2,X0,X1] : mult(rd(X0,X1),rd(mult(X1,X2),X1)) = rd(mult(X0,X2),X1),
inference(superposition,[],[f2195,f3]) ).
fof(f2918,plain,
! [X2,X3,X0,X1] : mult(mult(X0,rd(mult(X1,X2),X1)),mult(X1,X3)) = mult(X1,mult(ld(X1,mult(mult(X0,X1),X2)),X3)),
inference(superposition,[],[f48,f2195]) ).
fof(f2929,plain,
! [X2,X3,X0,X1] : mult(mult(X3,mult(X0,X2)),ld(mult(X0,X2),mult(X0,mult(X1,X2)))) = mult(X0,mult(ld(X0,mult(mult(X3,X0),X1)),X2)),
inference(backward_demodulation,[],[f18,f2918]) ).
fof(f3043,plain,
! [X2,X0,X1] : rd(mult(X2,X1),X2) = ld(rd(X0,X2),rd(mult(X0,X1),X2)),
inference(superposition,[],[f2,f2886]) ).
fof(f3152,plain,
! [X2,X0,X1] : rd(mult(ld(X0,X1),X2),ld(X0,X1)) = ld(X0,rd(mult(X1,X2),ld(X0,X1))),
inference(superposition,[],[f3043,f75]) ).
fof(f3172,plain,
! [X2,X0,X1] : rd(mult(X1,ld(X2,X0)),X1) = ld(rd(X2,X1),rd(X0,X1)),
inference(superposition,[],[f3043,f1]) ).
fof(f3188,plain,
! [X2,X0,X1] : rd(mult(X1,X2),X1) = ld(rd(rd(X0,X2),X1),rd(X0,X1)),
inference(superposition,[],[f3043,f3]) ).
fof(f3192,plain,
! [X0,X1] : rd(mult(X1,X0),X1) = ld(rd(unit,X1),rd(X0,X1)),
inference(superposition,[],[f3043,f6]) ).
fof(f3244,plain,
! [X0,X1] : rd(mult(x1,mult(X0,x1)),mult(X1,x1)) = ld(rd(mult(x0,X1),X1),rd(X0,X1)),
inference(backward_demodulation,[],[f2019,f3172]) ).
fof(f3286,plain,
! [X0,X1] : rd(mult(x1,mult(X0,x1)),mult(X1,x1)) = ld(x0,rd(X0,X1)),
inference(forward_demodulation,[],[f3244,f4]) ).
fof(f3311,plain,
! [X0] : ld(x0,rd(x0,X0)) = rd(mult(x1,unit),mult(X0,x1)),
inference(superposition,[],[f3286,f10]) ).
fof(f3312,plain,
! [X0,X1] : rd(mult(X0,x1),mult(X1,x1)) = ld(x0,rd(mult(x0,X0),X1)),
inference(superposition,[],[f3286,f494]) ).
fof(f3389,plain,
! [X0] : ld(x0,rd(x0,X0)) = rd(x1,mult(X0,x1)),
inference(forward_demodulation,[],[f3311,f5]) ).
fof(f3569,plain,
! [X0,X1] : rd(mult(X1,mult(X0,X1)),X1) = ld(rd(unit,X1),X0),
inference(superposition,[],[f3192,f4]) ).
fof(f3640,plain,
! [X0,X1] : rd(mult(rd(unit,X0),X1),rd(unit,X0)) = mult(rd(unit,X0),mult(X1,X0)),
inference(superposition,[],[f453,f70]) ).
fof(f3681,plain,
! [X0] : mult(x0,mult(x1,mult(X0,ld(ld(x1,unit),unit)))) = mult(x1,rd(mult(ld(x1,unit),X0),ld(x1,unit))),
inference(superposition,[],[f392,f453]) ).
fof(f3695,plain,
! [X0] : mult(mult(X0,ld(x0,unit)),x1) = mult(x1,mult(rd(mult(x0,X0),x0),x1)),
inference(superposition,[],[f494,f453]) ).
fof(f3706,plain,
! [X0] : mult(mult(X0,ld(x0,unit)),x1) = mult(x1,mult(x0,mult(X0,ld(x0,x1)))),
inference(forward_demodulation,[],[f3695,f47]) ).
fof(f3719,plain,
! [X0] : mult(x0,mult(x1,mult(X0,ld(ld(x1,unit),unit)))) = mult(x1,ld(x1,rd(mult(unit,X0),ld(x1,unit)))),
inference(forward_demodulation,[],[f3681,f3152]) ).
fof(f3743,plain,
! [X0,X1] : rd(unit,mult(rd(unit,X0),ld(X1,X0))) = mult(rd(unit,X0),mult(X1,X0)),
inference(forward_demodulation,[],[f3640,f1262]) ).
fof(f3751,plain,
! [X0] : mult(mult(X0,x1),mult(unit,x1)) = mult(x1,mult(x0,mult(X0,ld(x0,x1)))),
inference(forward_demodulation,[],[f3706,f513]) ).
fof(f3762,plain,
! [X0] : rd(mult(unit,X0),ld(x1,unit)) = mult(x0,mult(x1,mult(X0,ld(ld(x1,unit),unit)))),
inference(forward_demodulation,[],[f3719,f1]) ).
fof(f3788,plain,
! [X0] : mult(mult(X0,x1),x1) = mult(x1,mult(x0,mult(X0,ld(x0,x1)))),
inference(forward_demodulation,[],[f3751,f6]) ).
fof(f3797,plain,
! [X0] : rd(X0,ld(x1,unit)) = mult(x0,mult(x1,mult(X0,ld(ld(x1,unit),unit)))),
inference(forward_demodulation,[],[f3762,f6]) ).
fof(f3851,plain,
! [X0] : mult(x1,mult(x0,X0)) = mult(mult(rd(X0,ld(x0,x1)),x1),x1),
inference(superposition,[],[f3788,f3]) ).
fof(f3929,plain,
! [X0,X1] : mult(mult(x0,mult(x1,X0)),X1) = mult(x0,mult(x1,mult(X0,ld(x1,ld(x0,X1))))),
inference(superposition,[],[f2336,f47]) ).
fof(f3980,plain,
! [X0,X1] : mult(mult(x0,mult(x1,X0)),X1) = mult(x0,mult(x1,mult(X0,mult(mult(X1,x0),x1)))),
inference(forward_demodulation,[],[f3929,f1005]) ).
fof(f4217,plain,
! [X0,X1] : rd(X0,ld(X0,X1)) = mult(rd(unit,rd(X1,X0)),X0),
inference(superposition,[],[f722,f6]) ).
fof(f4232,plain,
! [X2,X0,X1] : rd(mult(X1,X2),X0) = mult(rd(X1,rd(mult(X2,X0),X2)),X2),
inference(superposition,[],[f722,f2]) ).
fof(f4361,plain,
! [X2,X0,X1] : rd(X0,rd(mult(X1,X2),X1)) = rd(rd(mult(X0,X1),X2),X1),
inference(superposition,[],[f4,f4232]) ).
fof(f4713,plain,
! [X2,X0,X1] : ld(ld(X1,X2),X2) = ld(mult(X0,ld(X1,X2)),mult(mult(X0,X1),ld(X1,X2))),
inference(superposition,[],[f2,f49]) ).
fof(f4744,plain,
! [X2,X0,X1] : ld(ld(X1,X2),X2) = ld(ld(X1,X2),mult(ld(X0,mult(X0,X1)),ld(X1,X2))),
inference(forward_demodulation,[],[f4713,f86]) ).
fof(f4771,plain,
! [X2,X0,X1] : ld(ld(X1,X2),X2) = ld(X2,mult(mult(X1,ld(X0,mult(X0,X1))),ld(X1,X2))),
inference(forward_demodulation,[],[f4744,f80]) ).
fof(f4786,plain,
! [X2,X1] : ld(ld(X1,X2),X2) = ld(X2,mult(mult(X1,X1),ld(X1,X2))),
inference(forward_demodulation,[],[f4771,f2]) ).
fof(f4823,plain,
ld(ld(x1,unit),unit) = ld(unit,mult(mult(x1,x0),x1)),
inference(superposition,[],[f4786,f22]) ).
fof(f4858,plain,
mult(mult(x1,x0),x1) = ld(ld(x1,unit),unit),
inference(forward_demodulation,[],[f4823,f51]) ).
fof(f4882,plain,
! [X0] : rd(X0,ld(x1,unit)) = mult(x0,mult(x1,mult(X0,mult(mult(x1,x0),x1)))),
inference(backward_demodulation,[],[f3797,f4858]) ).
fof(f4894,plain,
! [X0] : rd(X0,ld(x1,unit)) = mult(mult(x0,mult(x1,X0)),x1),
inference(forward_demodulation,[],[f4882,f3980]) ).
fof(f5099,plain,
! [X0,X1] : rd(mult(X0,X1),X0) = ld(rd(rd(X0,X1),X0),unit),
inference(superposition,[],[f3188,f77]) ).
fof(f5571,plain,
! [X2,X3,X0,X1] : mult(X2,mult(ld(X2,mult(mult(X1,X2),rd(X0,X3))),X3)) = mult(mult(X1,mult(X2,X3)),ld(mult(X2,X3),mult(X2,X0))),
inference(superposition,[],[f2929,f3]) ).
fof(f6208,plain,
! [X0] : mult(mult(X0,x1),ld(x1,unit)) = mult(mult(X0,ld(x1,unit)),mult(mult(x1,x0),x1)),
inference(superposition,[],[f49,f4858]) ).
fof(f6218,plain,
! [X0] : ld(ld(x1,unit),mult(X0,unit)) = mult(ld(ld(x1,unit),mult(X0,ld(x1,unit))),mult(mult(x1,x0),x1)),
inference(superposition,[],[f1691,f4858]) ).
fof(f6223,plain,
! [X0] : ld(ld(x1,unit),mult(X0,unit)) = mult(ld(unit,mult(mult(x1,X0),ld(x1,unit))),mult(mult(x1,x0),x1)),
inference(forward_demodulation,[],[f6218,f80]) ).
fof(f6231,plain,
! [X0] : mult(mult(X0,x0),x1) = mult(mult(X0,ld(x1,unit)),mult(mult(x1,x0),x1)),
inference(forward_demodulation,[],[f6208,f22]) ).
fof(f6234,plain,
! [X0] : ld(ld(x1,unit),mult(X0,unit)) = mult(mult(mult(x1,X0),ld(x1,unit)),mult(mult(x1,x0),x1)),
inference(forward_demodulation,[],[f6223,f51]) ).
fof(f6243,plain,
! [X0] : ld(ld(x1,unit),mult(X0,unit)) = mult(mult(mult(x1,X0),x0),x1),
inference(forward_demodulation,[],[f6234,f6231]) ).
fof(f6245,plain,
! [X0] : ld(ld(x1,unit),X0) = mult(mult(mult(x1,X0),x0),x1),
inference(forward_demodulation,[],[f6243,f5]) ).
fof(f7090,plain,
mult(rd(unit,x0),x1) = rd(x1,ld(x1,unit)),
inference(superposition,[],[f4894,f145]) ).
fof(f7954,plain,
! [X2,X3,X0,X1] : mult(ld(mult(X0,X1),X2),ld(X1,X3)) = ld(X1,mult(ld(X0,rd(X2,X1)),X3)),
inference(superposition,[],[f1691,f877]) ).
fof(f7963,plain,
! [X2,X3,X0,X1] : mult(rd(X3,rd(mult(ld(X0,rd(X2,X1)),X1),X1)),X1) = rd(mult(X3,X1),ld(mult(X0,X1),X2)),
inference(superposition,[],[f722,f877]) ).
fof(f7988,plain,
! [X2,X3,X0,X1] : rd(mult(X3,X1),ld(mult(X0,X1),X2)) = mult(rd(X3,ld(X0,rd(X2,X1))),X1),
inference(forward_demodulation,[],[f7963,f4]) ).
fof(f9427,plain,
! [X0,X1] : mult(rd(X0,ld(x0,X1)),x1) = rd(mult(X0,x1),mult(X1,x1)),
inference(superposition,[],[f4,f655]) ).
fof(f9463,plain,
! [X0,X1] : mult(rd(X0,ld(x0,X1)),x1) = ld(x0,rd(mult(x0,X0),X1)),
inference(forward_demodulation,[],[f9427,f3312]) ).
fof(f9512,plain,
! [X0,X1] : mult(rd(X0,ld(x0,X1)),x1) = rd(mult(X0,x1),mult(X1,x1)),
inference(backward_demodulation,[],[f3312,f9463]) ).
fof(f9913,plain,
! [X0] : rd(x0,ld(x0,rd(X0,x1))) = mult(rd(unit,mult(x0,mult(x1,X0))),x0),
inference(superposition,[],[f4217,f594]) ).
fof(f10321,plain,
rd(mult(x0,x1),x0) = ld(mult(x0,mult(x1,x0)),unit),
inference(superposition,[],[f5099,f594]) ).
fof(f10325,plain,
! [X2,X0,X1] : rd(mult(X2,rd(rd(X0,X1),X0)),X2) = rd(X2,mult(X2,rd(mult(X0,X1),X0))),
inference(superposition,[],[f1251,f5099]) ).
fof(f10355,plain,
! [X2,X0,X1] : rd(X2,mult(X2,rd(mult(X0,X1),X0))) = rd(mult(X2,rd(X0,X1)),mult(X2,X0)),
inference(forward_demodulation,[],[f10325,f1123]) ).
fof(f10359,plain,
mult(x0,mult(x1,x1)) = ld(mult(x0,mult(x1,x0)),unit),
inference(forward_demodulation,[],[f10321,f25]) ).
fof(f10388,plain,
rd(unit,x0) = ld(mult(x0,mult(x1,x0)),unit),
inference(forward_demodulation,[],[f10359,f145]) ).
fof(f11227,plain,
! [X0] : rd(rd(unit,X0),x1) = rd(x0,rd(mult(x1,X0),x1)),
inference(superposition,[],[f4361,f10]) ).
fof(f11286,plain,
! [X0] : rd(X0,rd(mult(x0,x1),x0)) = mult(x0,mult(x1,mult(X0,x0))),
inference(superposition,[],[f594,f4361]) ).
fof(f11293,plain,
! [X0] : mult(x0,mult(x1,mult(X0,x0))) = rd(X0,mult(x0,mult(x1,x1))),
inference(forward_demodulation,[],[f11286,f25]) ).
fof(f11321,plain,
! [X0] : rd(rd(unit,X0),x1) = rd(x0,ld(x0,rd(X0,x1))),
inference(forward_demodulation,[],[f11227,f1024]) ).
fof(f11348,plain,
! [X0] : rd(X0,rd(unit,x0)) = mult(x0,mult(x1,mult(X0,x0))),
inference(forward_demodulation,[],[f11293,f145]) ).
fof(f11361,plain,
! [X0] : rd(rd(unit,X0),x1) = mult(rd(unit,mult(x0,mult(x1,X0))),x0),
inference(backward_demodulation,[],[f9913,f11321]) ).
fof(f11522,plain,
! [X2,X0,X1] : ld(X2,mult(X0,X1)) = mult(X0,ld(ld(X0,mult(X2,X0)),X1)),
inference(superposition,[],[f2,f394]) ).
fof(f11854,plain,
! [X2,X0,X1] : mult(X1,ld(ld(X1,X0),X2)) = ld(rd(X0,X1),mult(X1,X2)),
inference(superposition,[],[f11522,f3]) ).
fof(f12352,plain,
! [X0,X1] : ld(rd(X1,X0),X0) = mult(X0,ld(ld(X0,X1),unit)),
inference(superposition,[],[f11854,f5]) ).
fof(f12813,plain,
mult(x0,ld(x1,unit)) = ld(rd(unit,x0),x0),
inference(superposition,[],[f12352,f66]) ).
fof(f13641,plain,
! [X0] : ld(X0,x1) = mult(ld(X0,mult(ld(x0,rd(x0,X0)),X0)),x1),
inference(superposition,[],[f1715,f3389]) ).
fof(f13665,plain,
! [X2,X0,X1] : ld(X0,mult(rd(X1,mult(X0,X2)),X0)) = rd(ld(X0,X1),X2),
inference(superposition,[],[f4,f1715]) ).
fof(f13802,plain,
! [X0] : ld(X0,x1) = mult(mult(ld(mult(x0,X0),x0),ld(X0,X0)),x1),
inference(forward_demodulation,[],[f13641,f7954]) ).
fof(f13906,plain,
! [X0] : ld(X0,x1) = mult(mult(ld(mult(x0,X0),x0),unit),x1),
inference(forward_demodulation,[],[f13802,f63]) ).
fof(f13961,plain,
! [X0] : ld(X0,x1) = mult(ld(mult(x0,X0),x0),x1),
inference(forward_demodulation,[],[f13906,f5]) ).
fof(f14987,plain,
! [X0] : rd(ld(x1,mult(X0,x1)),rd(unit,x0)) = mult(x0,mult(X0,mult(x1,x0))),
inference(superposition,[],[f11348,f174]) ).
fof(f15059,plain,
! [X0] : mult(x0,mult(X0,mult(x1,x0))) = rd(mult(mult(x0,X0),x1),rd(unit,x0)),
inference(forward_demodulation,[],[f14987,f24]) ).
fof(f15470,plain,
! [X2,X0,X1] : ld(X1,mult(rd(X0,X2),X1)) = rd(ld(X1,X0),ld(X1,X2)),
inference(superposition,[],[f1815,f3]) ).
fof(f15852,plain,
! [X0,X1] : rd(unit,ld(X0,X1)) = ld(X0,mult(rd(X0,X1),X0)),
inference(superposition,[],[f15470,f63]) ).
fof(f21784,plain,
! [X0,X1] : rd(unit,ld(mult(X0,X1),X0)) = ld(mult(X0,X1),mult(X0,mult(X1,ld(X0,mult(X0,X1))))),
inference(superposition,[],[f15852,f47]) ).
fof(f21894,plain,
! [X0,X1] : rd(unit,ld(mult(X0,X1),X0)) = ld(mult(X0,X1),mult(X0,mult(X1,X1))),
inference(forward_demodulation,[],[f21784,f2]) ).
fof(f22428,plain,
! [X2,X0,X1] : mult(rd(X1,mult(X0,X2)),X0) = mult(X0,rd(ld(X0,X1),X2)),
inference(superposition,[],[f1,f13665]) ).
fof(f22474,plain,
! [X0,X1] : rd(rd(ld(x1,X0),X1),x1) = mult(x0,rd(mult(rd(X0,mult(x1,X1)),x1),x1)),
inference(superposition,[],[f2236,f13665]) ).
fof(f22475,plain,
! [X0,X1] : rd(rd(ld(x1,X0),X1),x1) = mult(x0,rd(X0,mult(x1,X1))),
inference(forward_demodulation,[],[f22474,f4]) ).
fof(f22548,plain,
! [X0] : rd(rd(unit,X0),x1) = mult(x0,rd(ld(x0,unit),mult(x1,X0))),
inference(backward_demodulation,[],[f11361,f22428]) ).
fof(f22737,plain,
! [X0] : rd(rd(unit,X0),x1) = mult(x0,rd(x1,mult(x1,X0))),
inference(forward_demodulation,[],[f22548,f66]) ).
fof(f23395,plain,
! [X0] : rd(x1,mult(x1,X0)) = ld(x0,rd(rd(unit,X0),x1)),
inference(superposition,[],[f2,f22737]) ).
fof(f24233,plain,
mult(x1,mult(unit,x1)) = mult(mult(x1,x0),mult(rd(unit,x0),x1)),
inference(superposition,[],[f1957,f10388]) ).
fof(f24286,plain,
mult(x1,x1) = mult(mult(x1,x0),mult(rd(unit,x0),x1)),
inference(forward_demodulation,[],[f24233,f6]) ).
fof(f24505,plain,
rd(mult(mult(x1,x0),rd(unit,x0)),mult(x1,x0)) = rd(mult(x1,x1),mult(mult(x1,x0),x1)),
inference(superposition,[],[f1041,f24286]) ).
fof(f24560,plain,
rd(mult(mult(x1,x0),rd(unit,x0)),mult(x1,x0)) = mult(rd(x1,ld(x0,mult(x1,x0))),x1),
inference(forward_demodulation,[],[f24505,f9512]) ).
fof(f24578,plain,
rd(mult(mult(x1,x0),rd(unit,x0)),mult(x1,x0)) = mult(mult(rd(rd(x1,x0),x1),x0),x1),
inference(forward_demodulation,[],[f24560,f704]) ).
fof(f24589,plain,
rd(mult(mult(x1,x0),rd(unit,x0)),mult(x1,x0)) = mult(rd(x1,x0),ld(x1,mult(x0,x1))),
inference(forward_demodulation,[],[f24578,f72]) ).
fof(f24594,plain,
rd(mult(mult(x1,x0),rd(unit,x0)),mult(x1,x0)) = mult(rd(x1,x0),mult(mult(x0,x0),x1)),
inference(forward_demodulation,[],[f24589,f24]) ).
fof(f24598,plain,
rd(mult(mult(x1,x0),rd(unit,x0)),mult(x1,x0)) = mult(rd(x1,x0),ld(x1,unit)),
inference(forward_demodulation,[],[f24594,f137]) ).
fof(f24602,plain,
mult(rd(x1,x0),ld(x1,unit)) = rd(mult(mult(x1,x0),unit),mult(mult(x1,x0),x0)),
inference(forward_demodulation,[],[f24598,f1123]) ).
fof(f24604,plain,
mult(rd(x1,x0),ld(x1,unit)) = rd(mult(x1,x0),mult(mult(x1,x0),x0)),
inference(forward_demodulation,[],[f24602,f5]) ).
fof(f24608,plain,
mult(mult(x1,x0),x0) = ld(mult(rd(x1,x0),ld(x1,unit)),mult(x1,x0)),
inference(superposition,[],[f70,f24604]) ).
fof(f30115,plain,
! [X0,X1] : mult(x1,mult(x0,mult(mult(X0,ld(x0,x1)),X1))) = mult(mult(mult(X0,rd(mult(ld(x0,x1),X1),ld(x0,x1))),x1),x1),
inference(superposition,[],[f3851,f2195]) ).
fof(f30144,plain,
! [X0,X1] : mult(mult(X1,mult(rd(X0,ld(x0,x1)),x1)),x1) = mult(mult(X1,x1),ld(x1,mult(x1,mult(x0,X0)))),
inference(superposition,[],[f8,f3851]) ).
fof(f30202,plain,
! [X0,X1] : mult(mult(X1,x1),mult(x0,X0)) = mult(mult(X1,mult(rd(X0,ld(x0,x1)),x1)),x1),
inference(forward_demodulation,[],[f30144,f2]) ).
fof(f30218,plain,
! [X0,X1] : mult(x1,mult(x0,mult(mult(X0,ld(x0,x1)),X1))) = mult(mult(mult(X0,ld(x0,rd(mult(x1,X1),ld(x0,x1)))),x1),x1),
inference(forward_demodulation,[],[f30115,f3152]) ).
fof(f30243,plain,
! [X0,X1] : mult(x1,mult(x0,mult(mult(X0,ld(x0,x1)),X1))) = mult(mult(mult(X0,x1),mult(rd(mult(x1,X1),ld(x0,x1)),x1)),x1),
inference(forward_demodulation,[],[f30218,f513]) ).
fof(f30256,plain,
! [X0,X1] : mult(x1,mult(x0,mult(mult(X0,ld(x0,x1)),X1))) = mult(mult(mult(X0,x1),x1),mult(x0,mult(x1,X1))),
inference(forward_demodulation,[],[f30243,f30202]) ).
fof(f30510,plain,
! [X0,X1] : mult(mult(X0,x1),mult(x0,mult(x1,X1))) = mult(x1,mult(x0,mult(mult(rd(X0,x1),ld(x0,x1)),X1))),
inference(superposition,[],[f30256,f3]) ).
fof(f30521,plain,
! [X0,X1] : mult(x1,mult(x0,mult(mult(rd(X0,ld(x0,x1)),ld(x0,x1)),X1))) = mult(mult(x1,mult(x0,X0)),mult(x0,mult(x1,X1))),
inference(superposition,[],[f30256,f3851]) ).
fof(f30620,plain,
! [X0,X1] : mult(mult(x1,mult(x0,X0)),mult(x0,mult(x1,X1))) = mult(x1,mult(x0,mult(X0,X1))),
inference(forward_demodulation,[],[f30521,f3]) ).
fof(f31051,plain,
! [X0,X1] : mult(x1,mult(x0,mult(ld(x0,X0),X1))) = mult(mult(x1,X0),mult(x0,mult(x1,X1))),
inference(superposition,[],[f30620,f1]) ).
fof(f31347,plain,
! [X0] : mult(mult(X0,x1),mult(x0,mult(x1,x1))) = mult(x1,mult(x0,mult(X0,ld(x1,mult(ld(x0,x1),x1))))),
inference(superposition,[],[f30510,f72]) ).
fof(f31441,plain,
! [X0] : mult(mult(X0,x1),mult(x0,mult(x1,x1))) = mult(x1,mult(x0,mult(X0,mult(mult(x0,ld(x0,x1)),x1)))),
inference(forward_demodulation,[],[f31347,f24]) ).
fof(f31477,plain,
! [X0] : mult(mult(X0,x1),mult(x0,mult(x1,x1))) = mult(x1,mult(x0,mult(X0,mult(mult(x0,x1),mult(x1,x1))))),
inference(forward_demodulation,[],[f31441,f513]) ).
fof(f31503,plain,
! [X0] : mult(mult(X0,x1),mult(x0,mult(x1,x1))) = mult(x1,mult(x0,mult(X0,mult(unit,mult(x1,x1))))),
inference(forward_demodulation,[],[f31477,f10]) ).
fof(f31523,plain,
! [X0] : mult(mult(X0,x1),mult(x0,mult(x1,x1))) = mult(x1,mult(x0,mult(X0,mult(x1,x1)))),
inference(forward_demodulation,[],[f31503,f6]) ).
fof(f31536,plain,
! [X0] : mult(mult(X0,x1),rd(unit,x0)) = mult(x1,mult(x0,mult(X0,mult(x1,x1)))),
inference(forward_demodulation,[],[f31523,f145]) ).
fof(f31564,plain,
! [X0] : mult(mult(rd(X0,x1),x1),rd(unit,x0)) = mult(x1,mult(x0,mult(x1,mult(ld(x1,X0),x1)))),
inference(superposition,[],[f31536,f48]) ).
fof(f31656,plain,
! [X0] : mult(mult(rd(X0,x1),x1),rd(unit,x0)) = mult(x1,rd(ld(x1,X0),x0)),
inference(forward_demodulation,[],[f31564,f573]) ).
fof(f31680,plain,
! [X0] : mult(X0,rd(unit,x0)) = mult(x1,rd(ld(x1,X0),x0)),
inference(forward_demodulation,[],[f31656,f3]) ).
fof(f31726,plain,
! [X0] : mult(x1,rd(X0,x0)) = mult(mult(x1,X0),rd(unit,x0)),
inference(superposition,[],[f31680,f2]) ).
fof(f31737,plain,
! [X0] : rd(mult(X0,rd(unit,x0)),x1) = ld(x0,rd(rd(ld(x1,X0),x0),x1)),
inference(superposition,[],[f1024,f31680]) ).
fof(f31745,plain,
! [X0] : rd(ld(x1,X0),x0) = ld(x1,mult(X0,rd(unit,x0))),
inference(superposition,[],[f2,f31680]) ).
fof(f31801,plain,
! [X0] : rd(mult(X0,rd(unit,x0)),x1) = ld(x0,mult(x0,rd(X0,mult(x1,x0)))),
inference(forward_demodulation,[],[f31737,f22475]) ).
fof(f31821,plain,
! [X0] : rd(X0,mult(x1,x0)) = rd(mult(X0,rd(unit,x0)),x1),
inference(forward_demodulation,[],[f31801,f2]) ).
fof(f31905,plain,
! [X0] : rd(mult(mult(x1,X0),unit),mult(mult(x1,X0),x0)) = rd(mult(x1,rd(X0,x0)),mult(x1,X0)),
inference(superposition,[],[f1123,f31726]) ).
fof(f31966,plain,
! [X0] : rd(mult(mult(x1,X0),unit),mult(mult(x1,X0),x0)) = rd(x1,mult(x1,rd(mult(X0,x0),X0))),
inference(forward_demodulation,[],[f31905,f10355]) ).
fof(f31992,plain,
! [X0] : rd(mult(mult(x1,X0),unit),mult(mult(x1,X0),x0)) = rd(x1,mult(x1,rd(X0,mult(X0,x1)))),
inference(forward_demodulation,[],[f31966,f1191]) ).
fof(f32009,plain,
! [X0] : rd(x1,mult(x1,rd(X0,mult(X0,x1)))) = rd(mult(x1,X0),mult(mult(x1,X0),x0)),
inference(forward_demodulation,[],[f31992,f5]) ).
fof(f32022,plain,
mult(rd(x1,x0),ld(x1,unit)) = rd(x1,mult(x1,rd(x0,mult(x0,x1)))),
inference(backward_demodulation,[],[f24604,f32009]) ).
fof(f32028,plain,
mult(rd(x1,x0),ld(x1,unit)) = rd(x1,mult(x1,rd(x0,unit))),
inference(forward_demodulation,[],[f32022,f10]) ).
fof(f32030,plain,
rd(x1,mult(x1,x0)) = mult(rd(x1,x0),ld(x1,unit)),
inference(forward_demodulation,[],[f32028,f73]) ).
fof(f32032,plain,
mult(mult(x1,x0),x0) = ld(rd(x1,mult(x1,x0)),mult(x1,x0)),
inference(backward_demodulation,[],[f24608,f32030]) ).
fof(f32619,plain,
! [X0] : mult(X0,rd(mult(x1,rd(unit,x0)),x1)) = rd(mult(X0,x1),mult(x1,x0)),
inference(superposition,[],[f2195,f31821]) ).
fof(f32643,plain,
! [X0,X1] : mult(x1,ld(ld(x1,mult(X0,rd(unit,x0))),X1)) = ld(rd(X0,mult(x1,x0)),mult(x1,X1)),
inference(superposition,[],[f11854,f31821]) ).
fof(f32653,plain,
! [X0,X1] : ld(rd(X0,mult(x1,x0)),mult(x1,X1)) = mult(x1,ld(rd(ld(x1,X0),x0),X1)),
inference(forward_demodulation,[],[f32643,f31745]) ).
fof(f32672,plain,
! [X0] : mult(X0,rd(mult(x1,unit),mult(x1,x0))) = rd(mult(X0,x1),mult(x1,x0)),
inference(forward_demodulation,[],[f32619,f1123]) ).
fof(f32689,plain,
mult(mult(x1,x0),x0) = mult(x1,ld(rd(ld(x1,x1),x0),x0)),
inference(backward_demodulation,[],[f32032,f32653]) ).
fof(f32697,plain,
! [X0] : mult(X0,ld(x0,rd(rd(unit,x0),x1))) = rd(mult(X0,x1),mult(x1,x0)),
inference(forward_demodulation,[],[f32672,f1618]) ).
fof(f32704,plain,
mult(x1,ld(rd(unit,x0),x0)) = mult(mult(x1,x0),x0),
inference(forward_demodulation,[],[f32689,f63]) ).
fof(f32708,plain,
! [X0] : mult(X0,rd(x1,mult(x1,x0))) = rd(mult(X0,x1),mult(x1,x0)),
inference(forward_demodulation,[],[f32697,f23395]) ).
fof(f32710,plain,
mult(x1,mult(x0,ld(x1,unit))) = mult(mult(x1,x0),x0),
inference(forward_demodulation,[],[f32704,f12813]) ).
fof(f32713,plain,
rd(mult(x1,x0),x1) = mult(mult(x1,x0),x0),
inference(forward_demodulation,[],[f32710,f453]) ).
fof(f32715,plain,
rd(x1,mult(x1,x1)) = mult(mult(x1,x0),x0),
inference(forward_demodulation,[],[f32713,f1191]) ).
fof(f32716,plain,
ld(x0,rd(x0,x1)) = mult(mult(x1,x0),x0),
inference(forward_demodulation,[],[f32715,f3389]) ).
fof(f32763,plain,
! [X0] : mult(X0,x1) = mult(mult(X0,rd(x1,mult(x1,x0))),mult(x1,x0)),
inference(superposition,[],[f3,f32708]) ).
fof(f32802,plain,
! [X0] : mult(X0,x1) = mult(mult(X0,mult(x1,x0)),ld(mult(x1,x0),x1)),
inference(forward_demodulation,[],[f32763,f71]) ).
fof(f32840,plain,
mult(mult(mult(x1,x0),x0),x1) = mult(x1,mult(rd(x0,x1),x1)),
inference(superposition,[],[f554,f32716]) ).
fof(f32841,plain,
! [X0] : mult(x1,mult(mult(rd(x0,x1),x1),X0)) = mult(mult(mult(x1,x0),x0),mult(x1,X0)),
inference(superposition,[],[f631,f32716]) ).
fof(f32861,plain,
! [X0] : mult(rd(X0,x0),rd(rd(x0,x1),x0)) = rd(mult(X0,mult(mult(x1,x0),x0)),x0),
inference(superposition,[],[f2180,f32716]) ).
fof(f32886,plain,
! [X0] : mult(rd(X0,x0),mult(x0,mult(x1,x0))) = rd(mult(X0,mult(mult(x1,x0),x0)),x0),
inference(forward_demodulation,[],[f32861,f594]) ).
fof(f32900,plain,
! [X0] : mult(x1,mult(x0,X0)) = mult(mult(mult(x1,x0),x0),mult(x1,X0)),
inference(forward_demodulation,[],[f32841,f3]) ).
fof(f32901,plain,
mult(x1,x0) = mult(mult(mult(x1,x0),x0),x1),
inference(forward_demodulation,[],[f32840,f3]) ).
fof(f32908,plain,
! [X0] : mult(x0,mult(ld(x0,X0),mult(x1,x0))) = rd(mult(X0,mult(mult(x1,x0),x0)),x0),
inference(forward_demodulation,[],[f32886,f48]) ).
fof(f32918,plain,
mult(x1,x0) = ld(ld(x1,unit),x0),
inference(forward_demodulation,[],[f32901,f6245]) ).
fof(f32921,plain,
! [X0] : mult(x0,mult(x1,mult(mult(X0,x1),x0))) = rd(mult(X0,mult(mult(x1,x0),x0)),x0),
inference(forward_demodulation,[],[f32908,f631]) ).
fof(f32932,plain,
! [X0] : rd(mult(X0,x1),rd(unit,x0)) = rd(mult(X0,mult(mult(x1,x0),x0)),x0),
inference(forward_demodulation,[],[f32921,f11348]) ).
fof(f32964,plain,
rd(unit,ld(mult(mult(mult(x1,x0),x0),x1),mult(mult(x1,x0),x0))) = ld(mult(mult(mult(x1,x0),x0),x1),mult(x1,mult(x0,x1))),
inference(superposition,[],[f21894,f32900]) ).
fof(f33029,plain,
rd(unit,ld(mult(mult(mult(x1,x0),x0),x1),mult(mult(x1,x0),x0))) = mult(ld(mult(x0,mult(mult(mult(x1,x0),x0),x1)),x0),x1),
inference(forward_demodulation,[],[f32964,f2020]) ).
fof(f33089,plain,
rd(unit,ld(mult(mult(mult(x1,x0),x0),x1),mult(mult(x1,x0),x0))) = ld(mult(mult(mult(x1,x0),x0),x1),x1),
inference(forward_demodulation,[],[f33029,f13961]) ).
fof(f33122,plain,
rd(unit,ld(ld(ld(x1,unit),x0),mult(mult(x1,x0),x0))) = ld(ld(ld(x1,unit),x0),x1),
inference(forward_demodulation,[],[f33089,f6245]) ).
fof(f33144,plain,
rd(unit,ld(mult(x1,x0),mult(mult(x1,x0),x0))) = ld(mult(x1,x0),x1),
inference(forward_demodulation,[],[f33122,f32918]) ).
fof(f33157,plain,
rd(unit,x0) = ld(mult(x1,x0),x1),
inference(forward_demodulation,[],[f33144,f2]) ).
fof(f33172,plain,
! [X0] : mult(X0,x1) = mult(mult(X0,mult(x1,x0)),rd(unit,x0)),
inference(backward_demodulation,[],[f32802,f33157]) ).
fof(f33256,plain,
! [X0] : mult(X0,mult(x1,x0)) = rd(mult(X0,x1),rd(unit,x0)),
inference(superposition,[],[f4,f33172]) ).
fof(f33314,plain,
! [X0] : mult(X0,mult(x1,x0)) = rd(mult(X0,mult(mult(x1,x0),x0)),x0),
inference(backward_demodulation,[],[f32932,f33256]) ).
fof(f33320,plain,
! [X0] : mult(x0,mult(X0,mult(x1,x0))) = mult(mult(x0,X0),mult(x1,x0)),
inference(backward_demodulation,[],[f15059,f33256]) ).
fof(f33401,plain,
mult(x0,mult(x1,mult(x1,x0))) = mult(unit,mult(x1,x0)),
inference(superposition,[],[f33320,f10]) ).
fof(f33415,plain,
! [X0] : mult(rd(X0,x1),ld(x0,mult(x1,x0))) = ld(x0,mult(x0,mult(X0,mult(x1,x0)))),
inference(superposition,[],[f1998,f33320]) ).
fof(f33483,plain,
! [X0] : mult(X0,mult(x1,x0)) = mult(rd(X0,x1),ld(x0,mult(x1,x0))),
inference(forward_demodulation,[],[f33415,f2]) ).
fof(f33493,plain,
mult(x1,x0) = mult(x0,mult(x1,mult(x1,x0))),
inference(forward_demodulation,[],[f33401,f6]) ).
fof(f33517,plain,
mult(x1,x0) = rd(x1,rd(unit,x0)),
inference(forward_demodulation,[],[f33493,f11348]) ).
fof(f33779,plain,
! [X0] : mult(mult(X0,ld(x1,unit)),mult(x1,x0)) = mult(mult(X0,mult(x1,x0)),ld(mult(x1,x0),x0)),
inference(superposition,[],[f49,f32918]) ).
fof(f33780,plain,
ld(x1,unit) = rd(x0,mult(x1,x0)),
inference(superposition,[],[f75,f32918]) ).
fof(f33878,plain,
rd(mult(x1,x0),ld(mult(x1,x0),x0)) = mult(rd(unit,ld(x1,unit)),mult(x1,x0)),
inference(superposition,[],[f4217,f33780]) ).
fof(f33890,plain,
mult(x1,mult(x1,x0)) = rd(mult(x1,x0),ld(mult(x1,x0),x0)),
inference(forward_demodulation,[],[f33878,f75]) ).
fof(f33903,plain,
mult(x1,mult(x1,x0)) = mult(rd(x1,ld(x1,rd(x0,x0))),x0),
inference(forward_demodulation,[],[f33890,f7988]) ).
fof(f33909,plain,
mult(x1,mult(x1,x0)) = mult(rd(x1,ld(x1,unit)),x0),
inference(forward_demodulation,[],[f33903,f77]) ).
fof(f33913,plain,
mult(x1,mult(x1,x0)) = mult(mult(rd(unit,x0),x1),x0),
inference(forward_demodulation,[],[f33909,f7090]) ).
fof(f33915,plain,
mult(x1,mult(x1,x0)) = mult(unit,ld(x0,mult(x1,x0))),
inference(forward_demodulation,[],[f33913,f72]) ).
fof(f33919,plain,
mult(x1,mult(x1,x0)) = ld(x0,mult(x1,x0)),
inference(forward_demodulation,[],[f33915,f6]) ).
fof(f33929,plain,
! [X0] : mult(X0,mult(x1,x0)) = mult(rd(X0,x1),mult(x1,mult(x1,x0))),
inference(backward_demodulation,[],[f33483,f33919]) ).
fof(f33930,plain,
! [X0] : mult(X0,mult(x1,x0)) = mult(x1,mult(ld(x1,X0),mult(x1,x0))),
inference(forward_demodulation,[],[f33929,f48]) ).
fof(f33944,plain,
! [X0] : mult(mult(X0,x1),x0) = mult(mult(X0,x0),mult(x1,mult(x1,x0))),
inference(superposition,[],[f8,f33919]) ).
fof(f33953,plain,
! [X0] : mult(mult(X0,x0),mult(x1,mult(x1,x0))) = mult(mult(X0,mult(x1,mult(x1,x0))),ld(mult(x1,mult(x1,x0)),mult(x1,x0))),
inference(superposition,[],[f49,f33919]) ).
fof(f33997,plain,
! [X0] : mult(mult(X0,x0),mult(x1,mult(x1,x0))) = mult(x1,mult(ld(x1,mult(mult(X0,x1),rd(x0,mult(x1,x0)))),mult(x1,x0))),
inference(forward_demodulation,[],[f33953,f5571]) ).
fof(f34023,plain,
! [X0] : mult(mult(X0,x0),mult(x1,mult(x1,x0))) = mult(mult(mult(X0,x1),rd(x0,mult(x1,x0))),mult(x1,x0)),
inference(forward_demodulation,[],[f33997,f33930]) ).
fof(f34039,plain,
! [X0] : mult(mult(X0,x0),mult(x1,mult(x1,x0))) = mult(mult(mult(X0,x1),mult(x1,x0)),ld(mult(x1,x0),x0)),
inference(forward_demodulation,[],[f34023,f71]) ).
fof(f34048,plain,
! [X0] : mult(mult(X0,x0),mult(x1,mult(x1,x0))) = mult(mult(mult(X0,x1),ld(x1,unit)),mult(x1,x0)),
inference(forward_demodulation,[],[f34039,f33779]) ).
fof(f34054,plain,
! [X0] : mult(mult(X0,x0),mult(x1,mult(x1,x0))) = mult(mult(mult(X0,x0),x1),mult(x1,x0)),
inference(forward_demodulation,[],[f34048,f22]) ).
fof(f34057,plain,
! [X0] : mult(mult(X0,x1),x0) = mult(mult(mult(X0,x0),x1),mult(x1,x0)),
inference(forward_demodulation,[],[f34054,f33944]) ).
fof(f34267,plain,
! [X0] : mult(mult(X0,x1),mult(x1,x0)) = mult(mult(rd(X0,x0),x1),x0),
inference(superposition,[],[f34057,f3]) ).
fof(f34356,plain,
! [X0] : mult(mult(X0,x1),mult(x1,x0)) = mult(X0,ld(x0,mult(x1,x0))),
inference(forward_demodulation,[],[f34267,f72]) ).
fof(f34383,plain,
! [X0] : mult(mult(X0,x1),mult(x1,x0)) = mult(X0,mult(x1,mult(x1,x0))),
inference(forward_demodulation,[],[f34356,f33919]) ).
fof(f34464,plain,
! [X0,X1] : mult(rd(mult(X0,X1),X0),mult(x1,mult(x1,x0))) = mult(mult(X0,mult(X1,ld(X0,x1))),mult(x1,x0)),
inference(superposition,[],[f34383,f47]) ).
fof(f34544,plain,
! [X0,X1] : mult(mult(X0,mult(X1,ld(X0,x1))),mult(x1,x0)) = mult(X0,mult(X1,ld(X0,mult(x1,mult(x1,x0))))),
inference(forward_demodulation,[],[f34464,f47]) ).
fof(f36339,plain,
! [X0] : rd(mult(x1,X0),rd(unit,x0)) = mult(mult(x1,x0),rd(mult(rd(unit,x0),X0),rd(unit,x0))),
inference(superposition,[],[f2886,f33517]) ).
fof(f36367,plain,
! [X0] : rd(mult(x1,X0),rd(unit,x0)) = mult(mult(x1,x0),rd(unit,mult(rd(unit,x0),ld(X0,x0)))),
inference(forward_demodulation,[],[f36339,f1262]) ).
fof(f36387,plain,
! [X0] : rd(mult(x1,X0),rd(unit,x0)) = mult(mult(x1,x0),mult(rd(unit,x0),mult(X0,x0))),
inference(forward_demodulation,[],[f36367,f3743]) ).
fof(f36418,plain,
! [X0] : mult(rd(X0,mult(x1,x0)),mult(x1,x0)) = rd(mult(mult(x1,x0),mult(ld(mult(x1,x0),X0),x0)),x0),
inference(superposition,[],[f33314,f48]) ).
fof(f36507,plain,
! [X0] : mult(rd(X0,mult(x1,x0)),mult(x1,x0)) = mult(x1,rd(mult(x0,mult(ld(mult(x1,x0),X0),x0)),x0)),
inference(forward_demodulation,[],[f36418,f2195]) ).
fof(f36532,plain,
! [X0] : mult(rd(X0,mult(x1,x0)),mult(x1,x0)) = mult(x1,ld(rd(unit,x0),ld(mult(x1,x0),X0))),
inference(forward_demodulation,[],[f36507,f3569]) ).
fof(f36549,plain,
! [X0] : mult(x1,ld(rd(unit,x0),ld(mult(x1,x0),X0))) = X0,
inference(forward_demodulation,[],[f36532,f3]) ).
fof(f37346,plain,
! [X0] : mult(mult(x1,x0),X0) = mult(x1,ld(rd(unit,x0),X0)),
inference(superposition,[],[f36549,f2]) ).
fof(f37527,plain,
! [X0] : mult(x1,X0) = mult(mult(x1,x0),mult(rd(unit,x0),X0)),
inference(superposition,[],[f37346,f2]) ).
fof(f37623,plain,
! [X0] : mult(x1,mult(X0,x0)) = rd(mult(x1,X0),rd(unit,x0)),
inference(backward_demodulation,[],[f36387,f37527]) ).
fof(f37729,plain,
! [X0] : mult(rd(unit,x0),X0) = ld(mult(x1,x0),mult(x1,X0)),
inference(superposition,[],[f2,f37527]) ).
fof(f37998,plain,
! [X0] : mult(mult(x1,mult(X0,ld(x1,x1))),mult(x1,x0)) = mult(mult(x1,mult(X0,x0)),mult(rd(unit,x0),mult(x1,x0))),
inference(superposition,[],[f58,f37729]) ).
fof(f38063,plain,
! [X0] : mult(mult(x1,mult(X0,x0)),mult(rd(unit,x0),mult(x1,x0))) = mult(x1,mult(X0,ld(x1,mult(x1,mult(x1,x0))))),
inference(forward_demodulation,[],[f37998,f34544]) ).
fof(f38109,plain,
! [X0] : mult(x1,mult(X0,mult(x1,x0))) = mult(mult(x1,mult(X0,x0)),mult(rd(unit,x0),mult(x1,x0))),
inference(forward_demodulation,[],[f38063,f2]) ).
fof(f38373,plain,
! [X0,X1] : rd(mult(mult(x1,X0),X1),rd(unit,x0)) = mult(mult(x1,mult(X0,x0)),rd(mult(rd(unit,x0),X1),rd(unit,x0))),
inference(superposition,[],[f2886,f37623]) ).
fof(f38411,plain,
! [X0,X1] : rd(mult(mult(x1,X0),X1),rd(unit,x0)) = mult(mult(x1,mult(X0,x0)),rd(unit,mult(rd(unit,x0),ld(X1,x0)))),
inference(forward_demodulation,[],[f38373,f1262]) ).
fof(f38459,plain,
! [X0,X1] : rd(mult(mult(x1,X0),X1),rd(unit,x0)) = mult(mult(x1,mult(X0,x0)),mult(rd(unit,x0),mult(X1,x0))),
inference(forward_demodulation,[],[f38411,f3743]) ).
fof(f38485,plain,
! [X0] : mult(x1,mult(X0,mult(x1,x0))) = rd(mult(mult(x1,X0),x1),rd(unit,x0)),
inference(backward_demodulation,[],[f38109,f38459]) ).
fof(f38500,plain,
! [X0] : mult(mult(x1,X0),mult(x1,x0)) = mult(x1,mult(X0,mult(x1,x0))),
inference(forward_demodulation,[],[f38485,f33256]) ).
fof(f38542,plain,
! [X0,X1] : mult(x1,mult(mult(ld(x1,mult(X0,x1)),X1),mult(x1,x0))) = mult(mult(X0,mult(x1,X1)),mult(x1,x0)),
inference(superposition,[],[f38500,f174]) ).
fof(f38560,plain,
! [X0,X1] : mult(mult(x1,mult(X1,ld(x1,mult(x1,X0)))),mult(x1,x0)) = mult(mult(x1,mult(X1,x0)),ld(mult(x1,x0),mult(x1,mult(X0,mult(x1,x0))))),
inference(superposition,[],[f58,f38500]) ).
fof(f38627,plain,
! [X0,X1] : mult(mult(x1,mult(X1,ld(x1,mult(x1,X0)))),mult(x1,x0)) = mult(mult(x1,mult(X1,x0)),mult(rd(unit,x0),mult(X0,mult(x1,x0)))),
inference(forward_demodulation,[],[f38560,f37729]) ).
fof(f38638,plain,
! [X0,X1] : mult(mult(X0,mult(x1,X1)),mult(x1,x0)) = mult(x1,mult(mult(mult(mult(x0,X0),x1),X1),mult(x1,x0))),
inference(forward_demodulation,[],[f38542,f24]) ).
fof(f38663,plain,
! [X0,X1] : mult(mult(x1,mult(X1,x0)),mult(rd(unit,x0),mult(X0,mult(x1,x0)))) = mult(x1,mult(mult(X1,ld(x1,mult(x1,X0))),mult(x1,x0))),
inference(forward_demodulation,[],[f38627,f38500]) ).
fof(f38680,plain,
! [X0,X1] : mult(mult(x1,mult(X1,x0)),mult(rd(unit,x0),mult(X0,mult(x1,x0)))) = mult(x1,mult(mult(X1,X0),mult(x1,x0))),
inference(forward_demodulation,[],[f38663,f2]) ).
fof(f52165,plain,
! [X0,X1] : mult(x1,mult(x0,mult(ld(x0,X1),ld(x0,X0)))) = mult(mult(x1,X1),mult(rd(unit,x0),X0)),
inference(superposition,[],[f31051,f432]) ).
fof(f52274,plain,
! [X0,X1] : mult(mult(x1,X1),mult(rd(unit,x0),X0)) = mult(x1,mult(rd(X1,x0),X0)),
inference(forward_demodulation,[],[f52165,f177]) ).
fof(f52352,plain,
! [X0,X1] : mult(x1,mult(mult(X1,X0),mult(x1,x0))) = mult(x1,mult(rd(mult(X1,x0),x0),mult(X0,mult(x1,x0)))),
inference(backward_demodulation,[],[f38680,f52274]) ).
fof(f52404,plain,
! [X0,X1] : mult(x1,mult(mult(X1,X0),mult(x1,x0))) = mult(x1,mult(X1,mult(X0,mult(x1,x0)))),
inference(forward_demodulation,[],[f52352,f4]) ).
fof(f52457,plain,
! [X0,X1] : mult(mult(X0,mult(x1,X1)),mult(x1,x0)) = mult(x1,mult(mult(mult(x0,X0),x1),mult(X1,mult(x1,x0)))),
inference(backward_demodulation,[],[f38638,f52404]) ).
fof(f52497,plain,
! [X0,X1] : mult(mult(X0,mult(x1,X1)),mult(x1,x0)) = mult(X0,mult(x1,mult(X1,mult(x1,x0)))),
inference(forward_demodulation,[],[f52457,f489]) ).
fof(f52663,plain,
! [X0,X1] : mult(mult(X1,X0),mult(x1,x0)) = mult(X1,mult(x1,mult(ld(x1,X0),mult(x1,x0)))),
inference(superposition,[],[f52497,f1]) ).
fof(f52856,plain,
! [X0,X1] : mult(X1,mult(X0,mult(x1,x0))) = mult(mult(X1,X0),mult(x1,x0)),
inference(forward_demodulation,[],[f52663,f33930]) ).
fof(f52983,plain,
mult(x2,mult(x3,mult(x1,x0))) != mult(x2,mult(x3,mult(x1,x0))),
inference(backward_demodulation,[],[f11,f52856]) ).
fof(f52984,plain,
$false,
inference(trivial_inequality_removal,[],[f52983]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GRP664-12 : TPTP v9.3.1. Released v8.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.40 % Computer : n014.cluster.edu
% 0.12/0.40 % Model : x86_64 x86_64
% 0.12/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.40 % Memory : 8046.5625MB
% 0.12/0.40 % OS : Linux 6.8.0-71-generic
% 0.12/0.40 % CPULimit : 300
% 0.12/0.40 % WCLimit : 300
% 0.12/0.40 % DateTime : Sun Sep 27 10:33:03 UTC 2026
% 0.12/0.40 % CPUTime :
% 0.12/0.40 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.44 Running first-order theorem proving
% 0.12/0.44 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 130.09/19.12 % (599590)Detected a unit-equality problem, will run specialized UEQ schedule.
% 130.09/19.12 % (599602)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=128000:tgt=ground:npcc=on:spb=goal_then_units:urr=ec_only:random_seed=1266676016:i=130716:gtgl=4:add=on:doe=on:bd=all:gtg=exists_sym_3000 on theBenchmark for (3000ds/130716Mi)
% 130.09/19.12 % (599604)dis+10_14_to=lpo:sil=8000:tgt=full:drc=off:sp=const_frequency:sos=all:random_seed=1786609926:i=181:gtgl=5:bs=unit_only:fsr=off:gtg=exists_all_3000 on theBenchmark for (3000ds/181Mi)
% 130.09/19.12 % (599605)lrs+10_3_to=lpo:sil=64000:drc=off:fde=unused:sp=reverse_frequency:acc=on:bsr=on:fd=preordered:nwc=1:random_seed=1262721385:avsq=on:i=257:avsqr=16,3:bd=preordered:fsr=off_3000 on theBenchmark for (3000ds/257Mi)
% 130.09/19.12 % (599600)lrs+1002_1_ncem=casc2026/models/loop7.pt:sil=128000:tgt=ground:npcc=on:drc=off:sp=reverse_frequency:spb=goal:acc=on:s2agt=16:kmz=on:sac=on:random_seed=1992087150:i=138329:kws=inv_arity_squared:fgj=on:bd=preordered_3000 on theBenchmark for (3000ds/138329Mi)
% 130.09/19.12 % (599601)lrs+11_1_ncem=casc2026/models/loop6.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=2057946195:i=130792:sd=20:aac=none:nm=16:ss=included:sgt=10_3000 on theBenchmark for (3000ds/130792Mi)
% 130.09/19.12 % (599603)ott-1010_1_sfv=off:to=lpo:sil=8000:fdtod=off:sp=reverse_frequency:spb=goal_then_units:fd=preordered:random_seed=2386542227:i=136:bd=preordered:ins=2:av=off_3000 on theBenchmark for (3000ds/136Mi)
% 130.09/19.12 % (599606)dis-1010_7_sil=8000:fde=unused:flr=on:random_seed=3045874661:i=1187:sd=4:av=off:ss=axioms:sgt=32_3000 on theBenchmark for (3000ds/1187Mi)
% 130.09/19.12 % (599604)Instruction limit reached!
% 130.09/19.12 % (599604)------------------------------
% 130.09/19.12 % (599604)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 130.09/19.12 % (599604)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 130.09/19.12 % (599604)CaDiCaL version: 2.1.3
% 130.09/19.12 % (599604)Termination reason: Instruction limit
% 130.09/19.12 % (599604)Termination phase: Saturation
% 130.09/19.12 % (599604)Time elapsed: 0.145 s
% 130.09/19.12 % (599604)Peak memory usage: 89 MB
% 130.09/19.12 % (599604)Instructions burned: 181 (million)
% 130.09/19.12 % (599603)Instruction limit reached!
% 130.09/19.12 % (599603)------------------------------
% 130.09/19.12 % (599603)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 130.09/19.12 % (599603)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 130.09/19.12 % (599603)CaDiCaL version: 2.1.3
% 130.09/19.12 % (599603)Termination reason: Instruction limit
% 130.09/19.12 % (599603)Termination phase: Saturation
% 130.09/19.12 % (599603)Time elapsed: 0.129 s
% 130.09/19.12 % (599603)Peak memory usage: 88 MB
% 130.09/19.12 % (599603)Instructions burned: 136 (million)
% 130.09/19.12 % (599605)Instruction limit reached!
% 130.09/19.12 % (599605)------------------------------
% 130.09/19.12 % (599605)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 130.09/19.12 % (599605)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 130.09/19.12 % (599605)CaDiCaL version: 2.1.3
% 130.09/19.12 % (599605)Termination reason: Instruction limit
% 130.09/19.12 % (599605)Termination phase: Saturation
% 130.09/19.12 % (599605)Time elapsed: 0.161 s
% 130.09/19.12 % (599605)Peak memory usage: 90 MB
% 130.09/19.12 % (599605)Instructions burned: 257 (million)
% 130.09/19.12 % (599618)lrs+10_5:1_sil=8000:sos=all:urr=on:br=off:flr=on:random_seed=693073736:i=215:ep=RSTC_2996 on theBenchmark for (2996ds/215Mi)
% 130.09/19.12 % (599616)lrs-1011_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:prc=on:fde=unused:lcm=predicate:bsr=on:flr=on:random_seed=2894935719:i=2051:gtgl=2:fgj=on:bd=all:gtg=exists_top_2996 on theBenchmark for (2996ds/2051Mi)
% 130.09/19.12 % (599617)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3920076492:i=4948:ss=axioms:sgt=16_2996 on theBenchmark for (2996ds/4948Mi)
% 130.09/19.12 % (599618)Instruction limit reached!
% 130.09/19.12 % (599618)------------------------------
% 130.09/19.12 % (599618)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 130.09/19.12 % (599618)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 130.09/19.12 % (599618)CaDiCaL version: 2.1.3
% 130.09/19.12 % (599618)Termination reason: Instruction limit
% 130.09/19.12 % (599618)Termination phase: Saturation
% 130.09/19.12 % (599618)Time elapsed: 0.108 s
% 130.09/19.12 % (599618)Peak memory usage: 92 MB
% 130.09/19.12 % (599618)Instructions burned: 217 (million)
% 159.21/23.17 % (599625)lrs+11_1_sil=16000:tgt=full:fde=none:sp=reverse_frequency:lma=off:fs=off:acc=on:bsr=unit_only:rp=on:random_seed=2200988216:avsq=on:i=317:avsqr=1,16:kws=arity_squared:add=off:fgj=on:ins=10:fsr=off:gtg=exists_sym_2994 on theBenchmark for (2994ds/317Mi)
% 159.21/23.17 % (599625)Instruction limit reached!
% 159.21/23.17 % (599625)------------------------------
% 159.21/23.17 % (599625)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 159.21/23.17 % (599625)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 159.21/23.17 % (599625)CaDiCaL version: 2.1.3
% 159.21/23.17 % (599625)Termination reason: Instruction limit
% 159.21/23.17 % (599625)Termination phase: Saturation
% 159.21/23.17 % (599625)Time elapsed: 0.156 s
% 159.21/23.17 % (599625)Peak memory usage: 94 MB
% 159.21/23.17 % (599625)Instructions burned: 318 (million)
% 159.21/23.17 % (599628)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:sp=arity:lcm=predicate:urr=on:s2agt=16:br=off:random_seed=2708354311:i=12125:sd=2:fgj=on:ss=axioms:sgt=64_2990 on theBenchmark for (2990ds/12125Mi)
% 159.21/23.17 % (599606)Instruction limit reached!
% 159.21/23.17 % (599606)------------------------------
% 159.21/23.17 % (599606)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 159.21/23.17 % (599606)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 159.21/23.17 % (599606)CaDiCaL version: 2.1.3
% 159.21/23.17 % (599606)Termination reason: Instruction limit
% 159.21/23.17 % (599606)Termination phase: Saturation
% 159.21/23.17 % (599606)Time elapsed: 1.087 s
% 159.21/23.17 % (599606)Peak memory usage: 101 MB
% 159.21/23.17 % (599606)Instructions burned: 1187 (million)
% 159.21/23.17 % (599630)lrs+10_32_sil=8000:tgt=ground:prc=on:sp=reverse_arity:spb=non_intro:random_seed=166396882:i=2836:kws=inv_precedence:fgj=on:bd=preordered:ins=10_2986 on theBenchmark for (2986ds/2836Mi)
% 159.21/23.17 % (599616)Instruction limit reached!
% 159.21/23.17 % (599616)------------------------------
% 159.21/23.17 % (599616)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 159.21/23.17 % (599616)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 159.21/23.17 % (599616)CaDiCaL version: 2.1.3
% 159.21/23.17 % (599616)Termination reason: Instruction limit
% 159.21/23.17 % (599616)Termination phase: Saturation
% 159.21/23.17 % (599616)Time elapsed: 1.364 s
% 159.21/23.17 % (599616)Peak memory usage: 142 MB
% 159.21/23.17 % (599616)Instructions burned: 2052 (million)
% 159.21/23.17 % (599633)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=3499778979:i=14534:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2981 on theBenchmark for (2981ds/14534Mi)
% 159.21/23.17 % (599630)Instruction limit reached!
% 159.21/23.17 % (599630)------------------------------
% 159.21/23.17 % (599630)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 159.21/23.17 % (599630)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 159.21/23.17 % (599630)CaDiCaL version: 2.1.3
% 159.21/23.17 % (599630)Termination reason: Instruction limit
% 159.21/23.17 % (599630)Termination phase: Saturation
% 159.21/23.17 % (599630)Time elapsed: 3.160 s
% 159.21/23.17 % (599630)Peak memory usage: 132 MB
% 159.21/23.17 % (599630)Instructions burned: 2836 (million)
% 159.21/23.17 % (599638)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:sas=cadical:sp=reverse_frequency:bsr=on:alpa=false:sac=on:random_seed=880571447:i=11832:s2at=3:bs=on:bd=preordered:fsd=on_2953 on theBenchmark for (2953ds/11832Mi)
% 159.21/23.17 % (599617)Instruction limit reached!
% 159.21/23.17 % (599617)------------------------------
% 159.21/23.17 % (599617)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 159.21/23.17 % (599617)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 159.21/23.17 % (599617)CaDiCaL version: 2.1.3
% 159.21/23.17 % (599617)Termination reason: Instruction limit
% 159.21/23.17 % (599617)Termination phase: Saturation
% 159.21/23.17 % (599617)Time elapsed: 5.059 s
% 159.21/23.17 % (599617)Peak memory usage: 169 MB
% 159.21/23.17 % (599617)Instructions burned: 4948 (million)
% 159.21/23.17 % (599642)lrs+10_1_to=lpo:ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:drc=off:fde=unused:sp=const_min:spb=goal:fd=preordered:random_seed=1512365123:i=2279:fgj=on:bd=all_2943 on theBenchmark for (2943ds/2279Mi)
% 159.21/23.17 % (599642)Instruction limit reached!
% 159.21/23.17 % (599642)------------------------------
% 159.21/23.17 % (599642)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 89.87/23.75 % (599642)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 89.87/23.75 % (599642)CaDiCaL version: 2.1.3
% 89.87/23.75 % (599642)Termination reason: Instruction limit
% 89.87/23.75 % (599642)Termination phase: Saturation
% 89.87/23.75 % (599642)Time elapsed: 2.049 s
% 89.87/23.75 % (599642)Peak memory usage: 138 MB
% 89.87/23.75 % (599642)Instructions burned: 2279 (million)
% 89.87/23.75 % (599648)lrs-1010_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:drc=off:fde=none:sp=reverse_arity:urr=ec_only:gs=on:s2agt=16:random_seed=1610208288:st=3:i=6225:bd=all:gtg=exists_all:ss=included:er=filter:sgt=10_2921 on theBenchmark for (2921ds/6225Mi)
% 89.87/23.75 % (599628)Instruction limit reached!
% 89.87/23.75 % (599628)------------------------------
% 89.87/23.75 % (599628)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 89.87/23.75 % (599628)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 89.87/23.75 % (599628)CaDiCaL version: 2.1.3
% 89.87/23.75 % (599628)Termination reason: Instruction limit
% 89.87/23.75 % (599628)Termination phase: Saturation
% 89.87/23.75 % (599628)Time elapsed: 7.249 s
% 89.87/23.75 % (599628)Peak memory usage: 244 MB
% 89.87/23.75 % (599628)Instructions burned: 12126 (million)
% 89.87/23.75 % (599650)lrs-1010_1_sil=32000:tgt=ground:etr=on:sp=const_frequency:spb=goal_then_units:rnwc=on:lwlo=on:random_seed=1763994978:lrd=on:i=21755:kws=frequency:fgj=on:bd=preordered:nm=4:ins=20:av=off_2916 on theBenchmark for (2916ds/21755Mi)
% 89.87/23.75 % (599648)Instruction limit reached!
% 89.87/23.75 % (599648)------------------------------
% 89.87/23.75 % (599648)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 89.87/23.75 % (599648)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 89.87/23.75 % (599648)CaDiCaL version: 2.1.3
% 89.87/23.75 % (599648)Termination reason: Instruction limit
% 89.87/23.75 % (599648)Termination phase: Saturation
% 89.87/23.75 % (599648)Time elapsed: 6.062 s
% 89.87/23.75 % (599648)Peak memory usage: 169 MB
% 89.87/23.75 % (599648)Instructions burned: 6225 (million)
% 89.87/23.75 % (599654)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:flr=on:random_seed=2058403799:s2pl=no:i=16427:s2at=1.5:bd=all:fsr=off_2858 on theBenchmark for (2858ds/16427Mi)
% 89.87/23.75 % (599633)Instruction limit reached!
% 89.87/23.75 % (599633)------------------------------
% 89.87/23.75 % (599633)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 89.87/23.75 % (599633)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 89.87/23.75 % (599633)CaDiCaL version: 2.1.3
% 89.87/23.75 % (599633)Termination reason: Instruction limit
% 89.87/23.75 % (599633)Termination phase: Saturation
% 89.87/23.75 % (599633)Time elapsed: 14.695 s
% 89.87/23.75 % (599633)Peak memory usage: 258 MB
% 89.87/23.75 % (599633)Instructions burned: 14535 (million)
% 89.87/23.75 % (599638)Instruction limit reached!
% 89.87/23.75 % (599638)------------------------------
% 89.87/23.75 % (599638)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 89.87/23.75 % (599638)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 89.87/23.75 % (599638)CaDiCaL version: 2.1.3
% 89.87/23.75 % (599638)Termination reason: Instruction limit
% 89.87/23.75 % (599638)Termination phase: Saturation
% 89.87/23.75 % (599638)Time elapsed: 11.908 s
% 89.87/23.75 % (599638)Peak memory usage: 233 MB
% 89.87/23.75 % (599638)Instructions burned: 11833 (million)
% 89.87/23.75 % (599809)lrs+1011_1_to=lpo:ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:drc=off:fde=none:sp=const_frequency:spb=goal:fd=preordered:random_seed=1762677889:i=9356:fgj=on:bd=preordered:av=off_2832 on theBenchmark for (2832ds/9356Mi)
% 89.87/23.75 % (599810)dis+10_6_sil=8000:tgt=ground:prc=on:drc=ordering:spb=non_intro:fd=preordered:foolp=on:slsqc=1:slsq=on:random_seed=657900707:i=2070:kws=inv_precedence:slsql=off:bd=all_2831 on theBenchmark for (2831ds/2070Mi)
% 89.87/23.75 % (599810)Instruction limit reached!
% 89.87/23.75 % (599810)------------------------------
% 89.87/23.75 % (599810)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 89.87/23.75 % (599810)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 89.87/23.75 % (599810)CaDiCaL version: 2.1.3
% 89.87/23.75 % (599810)Termination reason: Instruction limit
% 89.87/23.75 % (599810)Termination phase: Saturation
% 89.87/23.75 % (599810)Time elapsed: 1.265 s
% 89.87/23.75 % (599810)Peak memory usage: 127 MB
% 89.87/23.75 % (599810)Instructions burned: 2071 (million)
% 89.87/23.75 % (599813)lrs+1002_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=8000:tgt=ground:npcc=on:fde=unused:sp=const_min:urr=ec_only:s2agt=32:random_seed=1197508173:st=3:i=6461:fgj=on:bd=preordered:av=off:ss=axioms_2817 on theBenchmark for (2817ds/6461Mi)
% 89.87/23.75 % (599813)Refutation not found, incomplete strategy
% 89.87/23.75 % (599813)------------------------------
% 89.87/23.75 % (599813)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 89.87/23.75 % (599813)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 89.87/23.75 % (599813)CaDiCaL version: 2.1.3
% 89.87/23.75 % (599813)Termination reason: Refutation not found, incomplete strategy
% 89.87/23.75 % (599813)Time elapsed: 0.570 s
% 89.87/23.75 % (599813)Peak memory usage: 127 MB
% 89.87/23.75 % (599813)Instructions burned: 858 (million)
% 89.87/23.75 % (599813)------------------------------
% 89.87/23.75 % (599813)------------------------------
% 89.87/23.75 % (599815)lrs+10_6_to=lpo:lpd=off:sil=8000:tgt=ground:drc=off:sp=arity:spb=goal:fd=preordered:random_seed=3130785636:i=2310:bd=all:ss=included_2808 on theBenchmark for (2808ds/2310Mi)
% 89.87/23.75 % (599650)Instruction limit reached!
% 89.87/23.75 % (599650)------------------------------
% 89.87/23.75 % (599650)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 89.87/23.75 % (599650)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 89.87/23.75 % (599650)CaDiCaL version: 2.1.3
% 89.87/23.75 % (599650)Termination reason: Instruction limit
% 89.87/23.75 % (599650)Termination phase: Saturation
% 89.87/23.75 % (599650)Time elapsed: 11.608 s
% 89.87/23.75 % (599650)Peak memory usage: 257 MB
% 89.87/23.75 % (599650)Instructions burned: 21757 (million)
% 89.87/23.75 % (599818)dis+11_1_sil=8000:fd=off:nwc=20:random_seed=2040713004:st=3:s2pl=on:i=2616:av=off:fsr=off:ss=axioms:sgt=8_2798 on theBenchmark for (2798ds/2616Mi)
% 89.87/23.75 % (599818)Refutation not found, incomplete strategy
% 89.87/23.75 % (599818)------------------------------
% 89.87/23.75 % (599818)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 89.87/23.75 % (599818)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 89.87/23.75 % (599818)CaDiCaL version: 2.1.3
% 89.87/23.75 % (599818)Termination reason: Refutation not found, incomplete strategy
% 89.87/23.75 % (599818)Time elapsed: 0.0000 s
% 89.87/23.75 % (599818)Peak memory usage: 87 MB
% 89.87/23.75 % (599818)------------------------------
% 89.87/23.75 % (599818)------------------------------
% 89.87/23.75 % (599815)Instruction limit reached!
% 89.87/23.75 % (599815)------------------------------
% 89.87/23.75 % (599815)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 89.87/23.75 % (599815)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 89.87/23.75 % (599815)CaDiCaL version: 2.1.3
% 89.87/23.75 % (599815)Termination reason: Instruction limit
% 89.87/23.75 % (599815)Termination phase: Saturation
% 89.87/23.75 % (599815)Time elapsed: 1.173 s
% 89.87/23.75 % (599815)Peak memory usage: 107 MB
% 89.87/23.75 % (599815)Instructions burned: 2311 (million)
% 89.87/23.75 % (599820)lrs+0_1_ncem=casc2026/models/loop3.pt:sil=32000:tgt=ground:npcc=on:sp=occurrence:urr=ec_only:fd=preordered:random_seed=3857373420:i=30521:gtgl=2:kws=inv_arity:bd=all:gtg=exists_sym_2795 on theBenchmark for (2795ds/30521Mi)
% 89.87/23.75 % (599822)lrs+11_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=16000:tgt=full:npcc=on:prc=on:fde=unused:sp=reverse_frequency:spb=goal:acc=on:urr=ec_only:s2agt=32:random_seed=1533318455:i=3258:fgj=on:bd=all:ins=1_2795 on theBenchmark for (2795ds/3258Mi)
% 89.87/23.75 % (599822)Instruction limit reached!
% 89.87/23.75 % (599822)------------------------------
% 89.87/23.75 % (599822)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 89.87/23.75 % (599822)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 89.87/23.75 % (599822)CaDiCaL version: 2.1.3
% 89.87/23.75 % (599822)Termination reason: Instruction limit
% 89.87/23.75 % (599822)Termination phase: Saturation
% 89.87/23.75 % (599822)Time elapsed: 1.722 s
% 89.87/23.75 % (599822)Peak memory usage: 141 MB
% 89.87/23.75 % (599822)Instructions burned: 3260 (million)
% 89.87/23.75 % (599809)Instruction limit reached!
% 89.87/23.75 % (599809)------------------------------
% 89.87/23.75 % (599809)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 89.87/23.75 % (599809)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 89.87/23.75 % (599809)CaDiCaL version: 2.1.3
% 89.87/23.75 % (599809)Termination reason: Instruction limit
% 89.87/23.75 % (599809)Termination phase: Saturation
% 89.87/23.75 % (599809)Time elapsed: 5.527 s
% 89.87/23.75 % (599809)Peak memory usage: 209 MB
% 89.87/23.75 % (599809)Instructions burned: 9356 (million)
% 89.87/23.75 % (599824)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:sp=reverse_frequency:kmz=on:random_seed=3631974052:i=5037:kws=precedence_2776 on theBenchmark for (2776ds/5037Mi)
% 89.87/23.75 % (599825)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:acc=on:urr=on:bsr=unit_only:br=off:random_seed=3078904538:i=65240_2775 on theBenchmark for (2775ds/65240Mi)
% 89.87/23.75 % (599654)First to succeed.
% 89.87/23.75 % (599654)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-599590"
% 89.87/23.75 % (599654)Refutation found. Thanks to Tanya!
% 89.87/23.75 % SZS status Unsatisfiable for theBenchmark
% 89.87/23.75 % SZS output start Proof for theBenchmark
% See solution above
% 163.51/23.84 % (599654)------------------------------
% 163.51/23.84 % (599654)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 163.51/23.84 % (599654)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 163.51/23.84 % (599654)CaDiCaL version: 2.1.3
% 163.51/23.84 % (599654)Termination reason: Refutation
% 163.51/23.84 % (599654)Time elapsed: 8.357 s
% 163.51/23.84 % (599654)Peak memory usage: 236 MB
% 163.51/23.84 % (599654)Instructions burned: 12462 (million)
% 163.51/23.84 % (599654)------------------------------
% 163.51/23.84 % (599654)------------------------------
% 163.51/23.84 % (599590)Success in time 22.994 s
% 163.51/23.84 % Vampire exiting
%------------------------------------------------------------------------------