%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GRP755-1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n026.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:16:07 AM UTC 2026
% Result : Unsatisfiable 12.87s 12.76s
% Output : Refutation 13.85s
% Verified :
% SZS Type : Refutation
% Derivation depth : 62
% Number of leaves : 10
% Syntax : Number of formulae : 112 ( 34 unt; 0 def)
% Number of atoms : 208 ( 207 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 101 ( 5 ~; 96 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 4 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 3 con; 0-2 aty)
% Number of variables : 216 ( 216 !; 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(mult(X0,X1),X2)
| mult(X0,mult(X1,X2)) = mult(mult(X0,X2),X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',f07) ).
fof(f8,axiom,
! [X2,X0,X1] :
( mult(X0,mult(X1,X2)) = mult(mult(X0,X1),X2)
| mult(X0,mult(X2,X1)) = mult(mult(X0,X1),X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',f08) ).
fof(f9,plain,
! [X2,X0,X1] :
( mult(X0,mult(X1,X2)) = mult(mult(X0,X1),X2)
| mult(mult(X0,X1),X2) = mult(X0,mult(X2,X1)) ),
inference(reorient_equations,[],[f8]) ).
fof(f10,axiom,
! [X0] : i(X0) = ld(X0,unit),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',f09) ).
fof(f11,negated_conjecture,
i(mult(a,b)) != mult(i(b),i(a)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goals) ).
fof(f12,plain,
ld(mult(a,b),unit) != mult(ld(b,unit),ld(a,unit)),
inference(definition_unfolding,[],[f11,f10,f10,f10]) ).
fof(f14,plain,
! [X0] : ld(unit,X0) = X0,
inference(superposition,[],[f6,f1]) ).
fof(f19,plain,
! [X0] : unit = ld(X0,X0),
inference(superposition,[],[f2,f5]) ).
fof(f21,plain,
! [X2,X0,X1] :
( mult(X1,mult(ld(X1,X0),X2)) = mult(mult(X1,X2),ld(X1,X0))
| mult(X0,X2) = mult(X1,mult(ld(X1,X0),X2)) ),
inference(superposition,[],[f7,f1]) ).
fof(f39,plain,
! [X0,X1] :
( mult(X0,mult(X1,X1)) != mult(X0,mult(X1,X1))
| mult(mult(X0,X1),X1) = mult(X0,mult(X1,X1)) ),
inference(equality_factoring,[],[f7]) ).
fof(f40,plain,
! [X0,X1] : mult(mult(X0,X1),X1) = mult(X0,mult(X1,X1)),
inference(trivial_inequality_removal,[],[f39]) ).
fof(f45,plain,
! [X0,X1] : mult(X1,mult(ld(X1,X0),ld(X1,X0))) = mult(X0,ld(X1,X0)),
inference(superposition,[],[f40,f1]) ).
fof(f91,plain,
! [X2,X0,X1] :
( mult(X0,X2) = mult(X1,mult(X2,ld(X1,X0)))
| mult(X0,X2) = mult(X1,mult(ld(X1,X0),X2)) ),
inference(superposition,[],[f9,f1]) ).
fof(f127,plain,
! [X0,X1] : mult(ld(X1,X0),ld(X1,X0)) = ld(X1,mult(X0,ld(X1,X0))),
inference(superposition,[],[f2,f45]) ).
fof(f142,plain,
! [X0] : mult(ld(X0,unit),ld(X0,unit)) = ld(X0,ld(X0,unit)),
inference(superposition,[],[f127,f6]) ).
fof(f173,plain,
! [X0,X1] : ld(rd(X0,X1),X0) = X1,
inference(superposition,[],[f2,f3]) ).
fof(f177,plain,
! [X2,X0,X1] :
( mult(X0,X2) = mult(rd(X0,X1),mult(X2,X1))
| mult(X0,X2) = mult(rd(X0,X1),mult(X1,X2)) ),
inference(superposition,[],[f9,f3]) ).
fof(f185,plain,
! [X0] : mult(X0,X0) = ld(rd(unit,X0),X0),
inference(superposition,[],[f142,f173]) ).
fof(f250,plain,
! [X0,X1] : rd(X0,ld(X1,X0)) = X1,
inference(superposition,[],[f4,f1]) ).
fof(f287,plain,
! [X0] : rd(unit,X0) = rd(X0,mult(X0,X0)),
inference(superposition,[],[f250,f185]) ).
fof(f374,plain,
! [X2,X0,X1] :
( mult(X0,X1) = mult(X2,mult(ld(X2,X0),X1))
| ld(X2,mult(X0,X1)) = mult(X1,ld(X2,X0)) ),
inference(superposition,[],[f2,f91]) ).
fof(f430,plain,
! [X2,X0,X1] :
( mult(ld(X2,X0),X1) = ld(X2,mult(X0,X1))
| ld(X2,mult(X0,X1)) = mult(X1,ld(X2,X0)) ),
inference(superposition,[],[f2,f374]) ).
fof(f469,plain,
! [X2,X0,X1] :
( ld(X1,X0) = mult(ld(X2,X0),ld(X1,X2))
| ld(X1,X0) = mult(ld(X1,X2),ld(X2,X0)) ),
inference(superposition,[],[f430,f1]) ).
fof(f487,plain,
! [X0,X1] :
( ld(X1,X0) = mult(X0,ld(X1,unit))
| ld(X1,X0) = mult(ld(X1,unit),X0) ),
inference(superposition,[],[f430,f6]) ).
fof(f582,plain,
! [X2,X0,X1] :
( ld(X2,X1) = ld(ld(X0,X2),ld(X0,X1))
| ld(X0,X1) = mult(ld(X2,X1),ld(X0,X2)) ),
inference(superposition,[],[f2,f469]) ).
fof(f789,plain,
! [X2,X0,X1] :
( mult(ld(X1,mult(X2,X0)),ld(X2,X1)) = X0
| ld(ld(X2,X1),X0) = ld(X1,mult(X2,X0)) ),
inference(superposition,[],[f582,f2]) ).
fof(f1028,plain,
! [X0,X1] :
( mult(mult(X0,X1),ld(X0,unit)) = X1
| mult(X0,X1) = ld(ld(X0,unit),X1) ),
inference(superposition,[],[f789,f14]) ).
fof(f1109,plain,
! [X0,X1] :
( mult(X1,mult(ld(X1,unit),X0)) = X0
| mult(unit,X0) = mult(X1,mult(ld(X1,unit),X0))
| mult(X1,X0) = ld(ld(X1,unit),X0) ),
inference(superposition,[],[f21,f1028]) ).
fof(f1117,plain,
! [X0,X1] :
( ld(X1,unit) = ld(mult(X1,X0),X0)
| mult(X1,X0) = ld(ld(X1,unit),X0) ),
inference(superposition,[],[f2,f1028]) ).
fof(f1136,plain,
! [X0,X1] :
( mult(X1,mult(ld(X1,unit),X0)) = X0
| mult(X1,mult(ld(X1,unit),X0)) = X0
| mult(X1,X0) = ld(ld(X1,unit),X0) ),
inference(forward_demodulation,[],[f1109,f6]) ).
fof(f1137,plain,
! [X0,X1] :
( mult(X1,mult(ld(X1,unit),X0)) = X0
| mult(X1,X0) = ld(ld(X1,unit),X0) ),
inference(duplicate_literal_removal,[],[f1136]) ).
fof(f1279,plain,
! [X0,X1] :
( ld(X1,unit) = ld(X0,ld(X1,X0))
| ld(ld(X1,unit),ld(X1,X0)) = X0 ),
inference(superposition,[],[f1117,f1]) ).
fof(f1529,plain,
! [X0,X1] :
( mult(X1,X0) = ld(ld(X1,unit),X0)
| ld(X1,X0) = mult(ld(X1,unit),X0) ),
inference(superposition,[],[f2,f1137]) ).
fof(f1583,plain,
! [X0,X1] :
( mult(ld(X0,unit),mult(X0,X1)) = X1
| ld(X0,X1) = mult(ld(X0,unit),X1) ),
inference(superposition,[],[f1,f1529]) ).
fof(f1648,plain,
! [X0,X1] :
( mult(ld(X1,unit),ld(X1,X0)) = ld(X1,ld(X1,X0))
| ld(X1,X0) = mult(ld(X1,unit),X0) ),
inference(superposition,[],[f1583,f1]) ).
fof(f1750,plain,
! [X0,X1] :
( ld(X0,X1) = ld(ld(X0,unit),ld(X0,ld(X0,X1)))
| ld(X0,X1) = mult(ld(X0,unit),X1) ),
inference(superposition,[],[f2,f1648]) ).
fof(f1790,plain,
! [X0,X1] :
( ld(ld(X1,unit),ld(X1,X0)) = X0
| mult(ld(X1,unit),mult(X1,X0)) = X0 ),
inference(superposition,[],[f1750,f2]) ).
fof(f1869,plain,
! [X0] :
( mult(ld(X0,unit),mult(X0,X0)) = X0
| ld(ld(X0,unit),unit) = X0 ),
inference(superposition,[],[f1790,f19]) ).
fof(f1949,plain,
! [X0] :
( ld(X0,unit) = rd(X0,mult(X0,X0))
| ld(ld(X0,unit),unit) = X0 ),
inference(superposition,[],[f4,f1869]) ).
fof(f1969,plain,
! [X0] :
( ld(ld(X0,unit),unit) = X0
| ld(X0,unit) = rd(unit,X0) ),
inference(forward_demodulation,[],[f1949,f287]) ).
fof(f2319,plain,
! [X0] :
( ld(X0,unit) = rd(unit,X0)
| ld(X0,unit) = rd(unit,X0) ),
inference(superposition,[],[f250,f1969]) ).
fof(f2340,plain,
! [X0] : ld(X0,unit) = rd(unit,X0),
inference(duplicate_literal_removal,[],[f2319]) ).
fof(f2361,plain,
! [X0] : unit = mult(ld(X0,unit),X0),
inference(superposition,[],[f3,f2340]) ).
fof(f2362,plain,
! [X0] : ld(ld(X0,unit),unit) = X0,
inference(superposition,[],[f250,f2340]) ).
fof(f2485,plain,
! [X0,X1] :
( mult(X0,X1) = mult(rd(X0,ld(X1,unit)),unit)
| mult(X0,X1) = mult(rd(X0,ld(X1,unit)),mult(X1,ld(X1,unit))) ),
inference(superposition,[],[f177,f2361]) ).
fof(f2486,plain,
! [X0,X1] :
( mult(X0,ld(X1,unit)) = mult(rd(X0,X1),unit)
| mult(X0,ld(X1,unit)) = mult(rd(X0,X1),mult(X1,ld(X1,unit))) ),
inference(superposition,[],[f177,f2361]) ).
fof(f2495,plain,
! [X0,X1] :
( mult(X1,unit) = mult(X0,ld(ld(X1,X0),unit))
| mult(X0,ld(ld(X1,X0),unit)) = mult(X1,mult(ld(X1,X0),ld(ld(X1,X0),unit))) ),
inference(superposition,[],[f91,f2361]) ).
fof(f2500,plain,
! [X0,X1] :
( mult(X0,ld(ld(X1,X0),unit)) = X1
| mult(X0,ld(ld(X1,X0),unit)) = mult(X1,mult(ld(X1,X0),ld(ld(X1,X0),unit))) ),
inference(forward_demodulation,[],[f2495,f5]) ).
fof(f2505,plain,
! [X0,X1] :
( rd(X0,X1) = mult(X0,ld(X1,unit))
| mult(X0,ld(X1,unit)) = mult(rd(X0,X1),mult(X1,ld(X1,unit))) ),
inference(forward_demodulation,[],[f2486,f5]) ).
fof(f2506,plain,
! [X0,X1] :
( mult(X0,X1) = rd(X0,ld(X1,unit))
| mult(X0,X1) = mult(rd(X0,ld(X1,unit)),mult(X1,ld(X1,unit))) ),
inference(forward_demodulation,[],[f2485,f5]) ).
fof(f2523,plain,
! [X0,X1] :
( mult(X1,unit) = mult(X0,ld(ld(X1,X0),unit))
| mult(X0,ld(ld(X1,X0),unit)) = X1 ),
inference(forward_demodulation,[],[f2500,f1]) ).
fof(f2524,plain,
! [X0,X1] :
( mult(X0,ld(X1,unit)) = mult(rd(X0,X1),unit)
| rd(X0,X1) = mult(X0,ld(X1,unit)) ),
inference(forward_demodulation,[],[f2505,f1]) ).
fof(f2525,plain,
! [X0,X1] :
( mult(X0,X1) = mult(rd(X0,ld(X1,unit)),unit)
| mult(X0,X1) = rd(X0,ld(X1,unit)) ),
inference(forward_demodulation,[],[f2506,f1]) ).
fof(f2530,plain,
! [X0,X1] :
( mult(X0,ld(ld(X1,X0),unit)) = X1
| mult(X0,ld(ld(X1,X0),unit)) = X1 ),
inference(forward_demodulation,[],[f2523,f5]) ).
fof(f2531,plain,
! [X0,X1] : mult(X0,ld(ld(X1,X0),unit)) = X1,
inference(duplicate_literal_removal,[],[f2530]) ).
fof(f2532,plain,
! [X0,X1] :
( rd(X0,X1) = mult(X0,ld(X1,unit))
| rd(X0,X1) = mult(X0,ld(X1,unit)) ),
inference(forward_demodulation,[],[f2524,f5]) ).
fof(f2533,plain,
! [X0,X1] : rd(X0,X1) = mult(X0,ld(X1,unit)),
inference(duplicate_literal_removal,[],[f2532]) ).
fof(f2534,plain,
! [X0,X1] :
( mult(X0,X1) = rd(X0,ld(X1,unit))
| mult(X0,X1) = rd(X0,ld(X1,unit)) ),
inference(forward_demodulation,[],[f2525,f5]) ).
fof(f2535,plain,
! [X0,X1] : mult(X0,X1) = rd(X0,ld(X1,unit)),
inference(duplicate_literal_removal,[],[f2534]) ).
fof(f2742,plain,
! [X0,X1] : ld(X1,X0) = ld(ld(X0,X1),unit),
inference(superposition,[],[f2,f2531]) ).
fof(f2837,plain,
! [X0,X1] : ld(X0,unit) = ld(mult(X1,X0),X1),
inference(superposition,[],[f2742,f2]) ).
fof(f2842,plain,
! [X0,X1] :
( ld(ld(X0,X1),X1) = ld(ld(X0,unit),unit)
| ld(ld(X0,unit),ld(X0,X1)) = X1 ),
inference(superposition,[],[f2742,f1279]) ).
fof(f2894,plain,
! [X2,X0,X1] : mult(X2,ld(X0,X1)) = rd(X2,ld(X1,X0)),
inference(superposition,[],[f2533,f2742]) ).
fof(f2952,plain,
! [X0,X1] :
( ld(ld(X0,X1),X1) = X0
| ld(ld(X0,unit),ld(X0,X1)) = X1 ),
inference(forward_demodulation,[],[f2842,f2362]) ).
fof(f2967,plain,
! [X0,X1] :
( ld(ld(X0,X1),X1) = ld(ld(X0,unit),unit)
| ld(X0,X1) = mult(ld(X0,unit),X1) ),
inference(superposition,[],[f2837,f487]) ).
fof(f3114,plain,
! [X0,X1] :
( ld(ld(X0,X1),X1) = X0
| ld(X0,X1) = mult(ld(X0,unit),X1) ),
inference(forward_demodulation,[],[f2967,f2362]) ).
fof(f3326,plain,
! [X0,X1] :
( mult(ld(X0,X1),X0) = X1
| ld(X0,X1) = mult(ld(X0,unit),X1) ),
inference(superposition,[],[f1,f3114]) ).
fof(f5186,plain,
! [X0,X1] :
( ld(ld(X0,X1),X1) = X0
| ld(ld(X0,X1),X1) = mult(ld(X0,X1),ld(ld(X0,X1),X0))
| ld(ld(X0,X1),X0) = mult(ld(ld(X0,X1),unit),X0) ),
inference(superposition,[],[f469,f3326]) ).
fof(f5195,plain,
! [X2,X0,X1] :
( mult(X1,X2) = mult(rd(X1,ld(X2,X0)),X0)
| mult(X1,X2) = mult(rd(X1,ld(X2,X0)),mult(X2,ld(X2,X0)))
| ld(X2,X0) = mult(ld(X2,unit),X0) ),
inference(superposition,[],[f177,f3326]) ).
fof(f5261,plain,
! [X2,X0,X1] :
( mult(X1,X2) = mult(mult(X1,ld(X0,X2)),X0)
| mult(X1,X2) = mult(rd(X1,ld(X2,X0)),mult(X2,ld(X2,X0)))
| ld(X2,X0) = mult(ld(X2,unit),X0) ),
inference(forward_demodulation,[],[f5195,f2894]) ).
fof(f5262,plain,
! [X0,X1] :
( ld(ld(X0,X1),X1) = X0
| ld(ld(X0,X1),X1) = X0
| ld(ld(X0,X1),X0) = mult(ld(ld(X0,X1),unit),X0) ),
inference(forward_demodulation,[],[f5186,f1]) ).
fof(f5263,plain,
! [X0,X1] :
( ld(ld(X0,X1),X1) = X0
| ld(ld(X0,X1),X0) = mult(ld(ld(X0,X1),unit),X0) ),
inference(duplicate_literal_removal,[],[f5262]) ).
fof(f5296,plain,
! [X2,X0,X1] :
( mult(X1,X2) = mult(rd(X1,ld(X2,X0)),X0)
| mult(X1,X2) = mult(mult(X1,ld(X0,X2)),X0)
| ld(X2,X0) = mult(ld(X2,unit),X0) ),
inference(forward_demodulation,[],[f5261,f1]) ).
fof(f5297,plain,
! [X0,X1] :
( ld(ld(X0,X1),X0) = mult(ld(X1,X0),X0)
| ld(ld(X0,X1),X1) = X0 ),
inference(forward_demodulation,[],[f5263,f2742]) ).
fof(f5311,plain,
! [X2,X0,X1] :
( mult(X1,X2) = mult(mult(X1,ld(X0,X2)),X0)
| mult(X1,X2) = mult(mult(X1,ld(X0,X2)),X0)
| ld(X2,X0) = mult(ld(X2,unit),X0) ),
inference(forward_demodulation,[],[f5296,f2894]) ).
fof(f5312,plain,
! [X2,X0,X1] :
( mult(X1,X2) = mult(mult(X1,ld(X0,X2)),X0)
| ld(X2,X0) = mult(ld(X2,unit),X0) ),
inference(duplicate_literal_removal,[],[f5311]) ).
fof(f5352,plain,
! [X0,X1] :
( ld(ld(X0,unit),ld(X0,X1)) = X1
| ld(ld(X0,unit),X1) = mult(ld(ld(X0,X1),X1),X1)
| ld(ld(X0,unit),ld(X0,X1)) = X1 ),
inference(superposition,[],[f5297,f1279]) ).
fof(f5544,plain,
! [X0,X1] :
( ld(ld(X0,unit),ld(X0,X1)) = X1
| ld(ld(X0,unit),X1) = mult(ld(ld(X0,X1),X1),X1) ),
inference(duplicate_literal_removal,[],[f5352]) ).
fof(f5962,plain,
! [X0,X1] :
( mult(X0,X1) = ld(ld(X0,unit),X1)
| ld(ld(X0,unit),ld(X0,X1)) = X1
| ld(ld(X0,unit),ld(X0,X1)) = X1 ),
inference(superposition,[],[f5544,f2952]) ).
fof(f6046,plain,
! [X0,X1] :
( ld(ld(X0,unit),ld(X0,X1)) = X1
| mult(X0,X1) = ld(ld(X0,unit),X1) ),
inference(duplicate_literal_removal,[],[f5962]) ).
fof(f6628,plain,
! [X0,X1] :
( mult(unit,X1) = mult(ld(X0,X1),X0)
| ld(X1,X0) = mult(ld(X1,unit),X0) ),
inference(superposition,[],[f5312,f6]) ).
fof(f6681,plain,
! [X0,X1] :
( mult(ld(X0,X1),X0) = X1
| ld(X1,X0) = mult(ld(X1,unit),X0) ),
inference(forward_demodulation,[],[f6628,f6]) ).
fof(f6837,plain,
! [X0,X1] :
( ld(ld(X0,X1),X1) = X0
| ld(ld(X0,X1),X1) = mult(ld(X0,X1),ld(ld(X0,X1),X0))
| ld(X0,ld(X0,X1)) = mult(ld(X0,unit),ld(X0,X1)) ),
inference(superposition,[],[f469,f6681]) ).
fof(f6921,plain,
! [X0,X1] :
( ld(ld(X0,X1),X1) = X0
| ld(ld(X0,X1),X1) = X0
| ld(X0,ld(X0,X1)) = mult(ld(X0,unit),ld(X0,X1)) ),
inference(forward_demodulation,[],[f6837,f1]) ).
fof(f6922,plain,
! [X0,X1] :
( ld(ld(X0,X1),X1) = X0
| ld(X0,ld(X0,X1)) = mult(ld(X0,unit),ld(X0,X1)) ),
inference(duplicate_literal_removal,[],[f6921]) ).
fof(f7066,plain,
! [X0,X1] :
( ld(ld(X1,unit),X0) = mult(ld(ld(X1,unit),unit),X0)
| ld(X1,unit) = ld(X0,ld(X1,X0))
| mult(X1,X0) = ld(ld(X1,unit),X0) ),
inference(superposition,[],[f6922,f6046]) ).
fof(f7210,plain,
! [X0,X1] :
( mult(X1,X0) = ld(ld(X1,unit),X0)
| ld(X1,unit) = ld(X0,ld(X1,X0))
| mult(X1,X0) = ld(ld(X1,unit),X0) ),
inference(forward_demodulation,[],[f7066,f2362]) ).
fof(f7211,plain,
! [X0,X1] :
( mult(X1,X0) = ld(ld(X1,unit),X0)
| ld(X1,unit) = ld(X0,ld(X1,X0)) ),
inference(duplicate_literal_removal,[],[f7210]) ).
fof(f7819,plain,
! [X0,X1] :
( rd(ld(X0,X1),ld(X0,unit)) = X1
| mult(X0,X1) = ld(ld(X0,unit),X1) ),
inference(superposition,[],[f250,f7211]) ).
fof(f7891,plain,
! [X0,X1] :
( mult(ld(X0,X1),X0) = X1
| mult(X0,X1) = ld(ld(X0,unit),X1) ),
inference(forward_demodulation,[],[f7819,f2535]) ).
fof(f8302,plain,
! [X0,X1] :
( ld(ld(X0,X1),X1) = X0
| ld(ld(X0,X1),X1) = mult(ld(X0,X1),ld(ld(X0,X1),X0))
| mult(ld(X0,X1),X0) = ld(ld(ld(X0,X1),unit),X0) ),
inference(superposition,[],[f469,f7891]) ).
fof(f8506,plain,
! [X0,X1] :
( ld(ld(X0,X1),X1) = X0
| ld(ld(X0,X1),X1) = X0
| mult(ld(X0,X1),X0) = ld(ld(ld(X0,X1),unit),X0) ),
inference(forward_demodulation,[],[f8302,f1]) ).
fof(f8507,plain,
! [X0,X1] :
( ld(ld(X0,X1),X1) = X0
| mult(ld(X0,X1),X0) = ld(ld(ld(X0,X1),unit),X0) ),
inference(duplicate_literal_removal,[],[f8506]) ).
fof(f8565,plain,
! [X0,X1] :
( mult(ld(X0,X1),X0) = ld(ld(X1,X0),X0)
| ld(ld(X0,X1),X1) = X0 ),
inference(forward_demodulation,[],[f8507,f2742]) ).
fof(f8642,plain,
! [X0,X1] :
( ld(X0,mult(X1,X0)) = X1
| mult(X0,X1) = ld(ld(mult(X1,X0),X1),X1) ),
inference(superposition,[],[f8565,f2]) ).
fof(f8973,plain,
! [X0,X1] :
( mult(X0,X1) = ld(ld(X0,unit),X1)
| ld(X0,mult(X1,X0)) = X1 ),
inference(forward_demodulation,[],[f8642,f2837]) ).
fof(f9123,plain,
! [X0,X1] :
( ld(ld(X0,unit),ld(X0,X1)) = X1
| mult(ld(X0,unit),X1) = ld(ld(ld(X0,unit),unit),X1)
| ld(X0,X1) = mult(ld(X0,unit),X1) ),
inference(superposition,[],[f8973,f487]) ).
fof(f9476,plain,
! [X0,X1] :
( ld(X0,X1) = mult(ld(X0,unit),X1)
| ld(ld(X0,unit),ld(X0,X1)) = X1
| ld(X0,X1) = mult(ld(X0,unit),X1) ),
inference(forward_demodulation,[],[f9123,f2362]) ).
fof(f9477,plain,
! [X0,X1] :
( ld(ld(X0,unit),ld(X0,X1)) = X1
| ld(X0,X1) = mult(ld(X0,unit),X1) ),
inference(duplicate_literal_removal,[],[f9476]) ).
fof(f9673,plain,
! [X0,X1] :
( ld(X1,X0) = mult(ld(X1,unit),X0)
| ld(X1,X0) = mult(ld(X1,unit),X0) ),
inference(superposition,[],[f1,f9477]) ).
fof(f9729,plain,
! [X0,X1] : ld(X1,X0) = mult(ld(X1,unit),X0),
inference(duplicate_literal_removal,[],[f9673]) ).
fof(f9852,plain,
ld(mult(a,b),unit) != ld(b,ld(a,unit)),
inference(superposition,[],[f12,f9729]) ).
fof(f9884,plain,
! [X0,X1] : ld(X1,unit) = ld(ld(X0,X1),ld(X0,unit)),
inference(superposition,[],[f2837,f9729]) ).
fof(f10828,plain,
! [X0,X1] : ld(X0,ld(X1,unit)) = ld(mult(X1,X0),unit),
inference(superposition,[],[f9884,f2]) ).
fof(f11658,plain,
ld(b,ld(a,unit)) != ld(b,ld(a,unit)),
inference(superposition,[],[f9852,f10828]) ).
fof(f11659,plain,
$false,
inference(trivial_inequality_removal,[],[f11658]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : GRP755-1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.07 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/10.40 % Computer : n026.cluster.edu
% 0.11/10.40 % Model : x86_64 x86_64
% 0.11/10.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/10.40 % Memory : 8046.5625MB
% 0.11/10.40 % OS : Linux 6.8.0-71-generic
% 0.11/10.40 % CPULimit : 300
% 0.11/10.40 % WCLimit : 300
% 0.11/10.40 % DateTime : Sun Sep 27 10:45:06 UTC 2026
% 0.11/10.41 % CPUTime :
% 0.11/10.41 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/10.44 Running first-order theorem proving
% 0.11/10.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
% 10.30/12.34 % (2647547)Input is clausal, will run a generic CNF schedule.
% 10.30/12.34 % (2647558)dis-21_1_sil=8000:lcm=predicate:random_seed=1031409409:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 10.30/12.34 % (2647558)Refutation not found, incomplete strategy
% 10.30/12.34 % (2647558)------------------------------
% 10.30/12.34 % (2647558)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.30/12.34 % (2647558)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.30/12.34 % (2647558)CaDiCaL version: 2.1.3
% 10.30/12.34 % (2647558)Termination reason: Refutation not found, incomplete strategy
% 10.30/12.34 % (2647558)Time elapsed: 0.001 s
% 10.30/12.34 % (2647558)Peak memory usage: 88 MB
% 10.30/12.34 % (2647554)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=1500766696:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 10.30/12.34 % (2647552)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=2380648304:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 10.30/12.34 % (2647555)lrs+10_1_sil=8000:sp=occurrence:random_seed=2652558128:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 10.30/12.34 % (2647556)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=1098740194:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 10.30/12.34 % (2647553)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=2464062008:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 10.30/12.34 % (2647557)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1838564526:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 10.30/12.34 % (2647555)Instruction limit reached!
% 10.30/12.34 % (2647555)------------------------------
% 10.30/12.34 % (2647555)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.30/12.34 % (2647555)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.30/12.34 % (2647555)CaDiCaL version: 2.1.3
% 10.30/12.34 % (2647555)Termination reason: Instruction limit
% 10.30/12.34 % (2647555)Termination phase: Saturation
% 10.30/12.34 % (2647555)Time elapsed: 0.062 s
% 10.30/12.34 % (2647555)Peak memory usage: 88 MB
% 10.30/12.34 % (2647555)Instructions burned: 107 (million)
% 10.30/12.34 % (2647556)Instruction limit reached!
% 10.30/12.34 % (2647556)------------------------------
% 10.30/12.34 % (2647556)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.30/12.34 % (2647556)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.30/12.34 % (2647556)CaDiCaL version: 2.1.3
% 10.30/12.34 % (2647556)Termination reason: Instruction limit
% 10.30/12.34 % (2647556)Termination phase: Saturation
% 10.30/12.34 % (2647556)Time elapsed: 0.068 s
% 10.30/12.34 % (2647556)Peak memory usage: 88 MB
% 10.30/12.34 % (2647556)Instructions burned: 116 (million)
% 10.30/12.34 % (2647558)------------------------------
% 10.30/12.34 % (2647558)------------------------------
% 10.30/12.34 % (2647557)Instruction limit reached!
% 10.30/12.34 % (2647557)------------------------------
% 10.30/12.34 % (2647557)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.30/12.34 % (2647557)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.30/12.34 % (2647557)CaDiCaL version: 2.1.3
% 10.30/12.34 % (2647557)Termination reason: Instruction limit
% 10.30/12.34 % (2647557)Termination phase: Saturation
% 10.30/12.34 % (2647557)Time elapsed: 0.102 s
% 10.30/12.34 % (2647557)Peak memory usage: 88 MB
% 10.30/12.34 % (2647557)Instructions burned: 180 (million)
% 10.30/12.34 % (2647567)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=3498270354:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2997 on theBenchmark for (2997ds/189Mi)
% 10.30/12.34 % (2647567)Refutation not found, incomplete strategy
% 10.30/12.34 % (2647567)------------------------------
% 10.30/12.34 % (2647567)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.30/12.34 % (2647567)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.30/12.34 % (2647567)CaDiCaL version: 2.1.3
% 10.30/12.34 % (2647567)Termination reason: Refutation not found, incomplete strategy
% 10.30/12.34 % (2647567)Time elapsed: 0.002 s
% 10.30/12.34 % (2647567)Peak memory usage: 88 MB
% 10.30/12.34 % (2647567)Instructions burned: 1 (million)
% 12.87/12.76 % (2647566)dis+1010_3_sil=8000:plsq=on:drc=off:fde=none:plsqc=1:bsd=on:plsqr=7,2:sos=on:spb=goal_then_units:random_seed=1441473604:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 12.87/12.76 % (2647568)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=1846181678:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 12.87/12.76 % (2647568)Refutation not found, incomplete strategy
% 12.87/12.76 % (2647568)------------------------------
% 12.87/12.76 % (2647568)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.87/12.76 % (2647568)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.87/12.76 % (2647568)CaDiCaL version: 2.1.3
% 12.87/12.76 % (2647568)Termination reason: Refutation not found, incomplete strategy
% 12.87/12.76 % (2647568)Time elapsed: 0.0000 s
% 12.87/12.76 % (2647568)Peak memory usage: 87 MB
% 12.87/12.76 % (2647566)Refutation not found, incomplete strategy
% 12.87/12.76 % (2647566)------------------------------
% 12.87/12.76 % (2647566)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.87/12.76 % (2647566)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.87/12.76 % (2647566)CaDiCaL version: 2.1.3
% 12.87/12.76 % (2647566)Termination reason: Refutation not found, incomplete strategy
% 12.87/12.76 % (2647566)Time elapsed: 0.001 s
% 12.87/12.76 % (2647566)Peak memory usage: 88 MB
% 12.87/12.76 % (2647569)lrs+10_64_to=lpo:sil=8000:random_seed=2883837728:i=126:bd=preordered_2997 on theBenchmark for (2997ds/126Mi)
% 12.87/12.76 % (2647569)Instruction limit reached!
% 12.87/12.76 % (2647569)------------------------------
% 12.87/12.76 % (2647569)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.87/12.76 % (2647569)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.87/12.76 % (2647569)CaDiCaL version: 2.1.3
% 12.87/12.76 % (2647569)Termination reason: Instruction limit
% 12.87/12.76 % (2647569)Termination phase: Saturation
% 12.87/12.76 % (2647569)Time elapsed: 0.076 s
% 12.87/12.76 % (2647569)Peak memory usage: 88 MB
% 12.87/12.76 % (2647569)Instructions burned: 126 (million)
% 12.87/12.76 % (2647568)------------------------------
% 12.87/12.76 % (2647568)------------------------------
% 12.87/12.76 % (2647567)------------------------------
% 12.87/12.76 % (2647567)------------------------------
% 12.87/12.76 % (2647575)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=4219538920:i=157:gtg=all_2995 on theBenchmark for (2995ds/157Mi)
% 12.87/12.76 % (2647574)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=97109857:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi)
% 12.87/12.76 % (2647566)------------------------------
% 12.87/12.76 % (2647566)------------------------------
% 12.87/12.76 % (2647575)Instruction limit reached!
% 12.87/12.76 % (2647575)------------------------------
% 12.87/12.76 % (2647575)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.87/12.76 % (2647575)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.87/12.76 % (2647575)CaDiCaL version: 2.1.3
% 12.87/12.76 % (2647575)Termination reason: Instruction limit
% 12.87/12.76 % (2647575)Termination phase: Saturation
% 12.87/12.76 % (2647575)Time elapsed: 0.049 s
% 12.87/12.76 % (2647575)Peak memory usage: 89 MB
% 12.87/12.76 % (2647575)Instructions burned: 160 (million)
% 12.87/12.76 % (2647574)Instruction limit reached!
% 12.87/12.76 % (2647574)------------------------------
% 12.87/12.76 % (2647574)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.87/12.76 % (2647574)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.87/12.76 % (2647574)CaDiCaL version: 2.1.3
% 12.87/12.76 % (2647574)Termination reason: Instruction limit
% 12.87/12.76 % (2647574)Termination phase: Saturation
% 12.87/12.76 % (2647574)Time elapsed: 0.109 s
% 12.87/12.76 % (2647574)Peak memory usage: 89 MB
% 12.87/12.76 % (2647574)Instructions burned: 194 (million)
% 12.87/12.76 % (2647580)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=1192079453:i=107_2993 on theBenchmark for (2993ds/107Mi)
% 12.87/12.76 % (2647578)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=2023179979:i=3394:sd=4:ss=included:sgt=64_2994 on theBenchmark for (2994ds/3394Mi)
% 12.87/12.76 % (2647580)Refutation not found, incomplete strategy
% 12.87/12.76 % (2647580)------------------------------
% 12.87/12.76 % (2647580)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.87/12.76 % (2647580)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.87/12.76 % (2647580)CaDiCaL version: 2.1.3
% 12.87/12.76 % (2647580)Termination reason: Refutation not found, incomplete strategy
% 12.87/12.76 % (2647580)Time elapsed: 0.001 s
% 12.87/12.76 % (2647580)Peak memory usage: 88 MB
% 12.87/12.76 % (2647579)lrs+1011_5_to=lpo:sil=8000:tgt=full:plsq=on:prc=on:drc=off:plsqr=31,4:sp=occurrence:urr=on:nwc=0.8:s2agt=16:br=off:random_seed=1355628483:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2994 on theBenchmark for (2994ds/106Mi)
% 12.87/12.76 % (2647579)Instruction limit reached!
% 12.87/12.76 % (2647579)------------------------------
% 12.87/12.76 % (2647579)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.87/12.76 % (2647579)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.87/12.76 % (2647579)CaDiCaL version: 2.1.3
% 12.87/12.76 % (2647579)Termination reason: Instruction limit
% 12.87/12.76 % (2647579)Termination phase: Saturation
% 12.87/12.76 % (2647579)Time elapsed: 0.057 s
% 12.87/12.76 % (2647579)Peak memory usage: 88 MB
% 12.87/12.76 % (2647579)Instructions burned: 107 (million)
% 12.87/12.76 % (2647581)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=100893639:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2993 on theBenchmark for (2993ds/242Mi)
% 12.87/12.76 % (2647580)------------------------------
% 12.87/12.76 % (2647580)------------------------------
% 12.87/12.76 % (2647585)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=3340681565:cond=fast:i=5208:av=off_2992 on theBenchmark for (2992ds/5208Mi)
% 12.87/12.76 % (2647581)Instruction limit reached!
% 12.87/12.76 % (2647581)------------------------------
% 12.87/12.76 % (2647581)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.87/12.76 % (2647581)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.87/12.76 % (2647581)CaDiCaL version: 2.1.3
% 12.87/12.76 % (2647581)Termination reason: Instruction limit
% 12.87/12.76 % (2647581)Termination phase: Saturation
% 12.87/12.76 % (2647581)Time elapsed: 0.139 s
% 12.87/12.76 % (2647581)Peak memory usage: 90 MB
% 12.87/12.76 % (2647581)Instructions burned: 242 (million)
% 12.87/12.76 % (2647587)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=1963390601:i=134:sd=2:doe=on:ss=axioms:sgt=14_2991 on theBenchmark for (2991ds/134Mi)
% 12.87/12.76 % (2647587)Instruction limit reached!
% 12.87/12.76 % (2647587)------------------------------
% 12.87/12.76 % (2647587)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.87/12.76 % (2647587)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.87/12.76 % (2647587)CaDiCaL version: 2.1.3
% 12.87/12.76 % (2647587)Termination reason: Instruction limit
% 12.87/12.76 % (2647587)Termination phase: Saturation
% 12.87/12.76 % (2647587)Time elapsed: 0.084 s
% 12.87/12.76 % (2647587)Peak memory usage: 89 MB
% 12.87/12.76 % (2647587)Instructions burned: 135 (million)
% 12.87/12.76 % (2647589)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=2371424121:i=499:bd=all_2990 on theBenchmark for (2990ds/499Mi)
% 12.87/12.76 % (2647591)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=474813812:i=191:fgj=on:bd=all_2989 on theBenchmark for (2989ds/191Mi)
% 12.87/12.76 % (2647591)Instruction limit reached!
% 12.87/12.76 % (2647591)------------------------------
% 12.87/12.76 % (2647591)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.87/12.76 % (2647591)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.87/12.76 % (2647591)CaDiCaL version: 2.1.3
% 12.87/12.76 % (2647591)Termination reason: Instruction limit
% 12.87/12.76 % (2647591)Termination phase: Saturation
% 12.87/12.76 % (2647591)Time elapsed: 0.114 s
% 12.87/12.76 % (2647591)Peak memory usage: 89 MB
% 12.87/12.76 % (2647591)Instructions burned: 191 (million)
% 12.87/12.76 % (2647589)Instruction limit reached!
% 12.87/12.76 % (2647589)------------------------------
% 12.87/12.76 % (2647589)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.87/12.76 % (2647589)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.87/12.76 % (2647589)CaDiCaL version: 2.1.3
% 12.87/12.76 % (2647589)Termination reason: Instruction limit
% 12.87/12.76 % (2647589)Termination phase: Saturation
% 12.87/12.76 % (2647589)Time elapsed: 0.265 s
% 12.87/12.76 % (2647589)Peak memory usage: 91 MB
% 12.87/12.76 % (2647589)Instructions burned: 500 (million)
% 12.87/12.76 % (2647595)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=3384567346:i=264:kws=precedence:fsr=off_2986 on theBenchmark for (2986ds/264Mi)
% 12.87/12.76 % (2647596)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=2081584046:cond=on:i=156:bs=on:gtg=exists_all:er=known_2986 on theBenchmark for (2986ds/156Mi)
% 12.87/12.76 % (2647596)Instruction limit reached!
% 12.87/12.76 % (2647596)------------------------------
% 12.87/12.76 % (2647596)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.87/12.76 % (2647596)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.87/12.76 % (2647596)CaDiCaL version: 2.1.3
% 12.87/12.76 % (2647596)Termination reason: Instruction limit
% 12.87/12.76 % (2647596)Termination phase: Saturation
% 12.87/12.76 % (2647596)Time elapsed: 0.098 s
% 12.87/12.76 % (2647596)Peak memory usage: 89 MB
% 12.87/12.76 % (2647596)Instructions burned: 156 (million)
% 12.87/12.76 % (2647553)First to succeed.
% 12.87/12.76 % (2647553)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2647547"
% 12.87/12.76 % (2647595)Instruction limit reached!
% 12.87/12.76 % (2647595)------------------------------
% 12.87/12.76 % (2647595)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.87/12.76 % (2647595)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.87/12.76 % (2647595)CaDiCaL version: 2.1.3
% 12.87/12.76 % (2647595)Termination reason: Instruction limit
% 12.87/12.76 % (2647595)Termination phase: Saturation
% 12.87/12.76 % (2647595)Time elapsed: 0.160 s
% 12.87/12.76 % (2647595)Peak memory usage: 91 MB
% 12.87/12.76 % (2647595)Instructions burned: 265 (million)
% 12.87/12.76 % (2647599)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=reverse_frequency:spb=units:lcm=predicate:urr=on:s2agt=8:updr=off:random_seed=3181049479:i=3256:kws=precedence:bd=preordered:av=off_2984 on theBenchmark for (2984ds/3256Mi)
% 12.87/12.76 % (2647600)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=182041814:i=537:av=off:ss=included_2983 on theBenchmark for (2983ds/537Mi)
% 12.87/12.76 % (2647553)Refutation found. Thanks to Tanya!
% 12.87/12.76 % SZS status Unsatisfiable for theBenchmark
% 12.87/12.76 % SZS output start Proof for theBenchmark
% See solution above
% 13.85/12.95 % (2647553)------------------------------
% 13.85/12.95 % (2647553)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.85/12.95 % (2647553)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.85/12.95 % (2647553)CaDiCaL version: 2.1.3
% 13.85/12.95 % (2647553)Termination reason: Refutation
% 13.85/12.95 % (2647553)Time elapsed: 1.469 s
% 13.85/12.95 % (2647553)Peak memory usage: 140 MB
% 13.85/12.95 % (2647553)Instructions burned: 2443 (million)
% 13.85/12.95 % (2647553)------------------------------
% 13.85/12.95 % (2647553)------------------------------
% 13.85/12.95 % (2647547)Success in time 1.875 s
% 13.85/12.95 % Vampire exiting
%------------------------------------------------------------------------------