%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : GRP683+1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n017.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:18:33 AM UTC 2026
% Result : Theorem 6.18s 1.42s
% Output : Refutation 6.18s
% Verified :
% SZS Type : Refutation
% Derivation depth : 58
% Number of leaves : 10
% Syntax : Number of formulae : 162 ( 145 unt; 2 def)
% Number of atoms : 179 ( 157 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 34 ( 17 ~; 13 |; 2 &)
% ( 2 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 3 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 4 ( 2 usr; 3 prp; 0-2 aty)
% Number of functors : 6 ( 6 usr; 3 con; 0-2 aty)
% Number of variables : 352 ( 0 sgn 349 !; 3 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0] : ld(X0,mult(X0,X0)) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',f01) ).
fof(f2,axiom,
! [X0] : rd(mult(X0,X0),X0) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',f02) ).
fof(f3,axiom,
! [X0,X1] : mult(X1,ld(X1,X0)) = ld(X1,mult(X1,X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',f03) ).
fof(f4,axiom,
! [X0,X1] : mult(rd(X1,X0),X0) = rd(mult(X1,X0),X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',f04) ).
fof(f5,axiom,
! [X0,X1,X2,X3] : ld(ld(X3,X2),mult(ld(X3,X2),mult(X1,X0))) = mult(ld(X3,mult(X3,X1)),X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',f05) ).
fof(f6,axiom,
! [X0,X1,X2,X3] : rd(mult(mult(X3,X2),rd(X1,X0)),rd(X1,X0)) = mult(X3,rd(mult(X2,X0),X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',f06) ).
fof(f7,axiom,
! [X0,X1] : ld(X1,mult(X1,ld(X0,X0))) = rd(mult(rd(X1,X1),X0),X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',f07) ).
fof(f8,conjecture,
! [X0,X1,X2] :
( mult(X0,ld(X1,mult(X1,X2))) = mult(X0,X2)
& mult(rd(mult(X0,X1),X1),X2) = mult(X0,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goals) ).
fof(f9,negated_conjecture,
~ ! [X0,X1,X2] :
( mult(X0,ld(X1,mult(X1,X2))) = mult(X0,X2)
& mult(rd(mult(X0,X1),X1),X2) = mult(X0,X2) ),
inference(negated_conjecture,[status(cth)],[f8]) ).
fof(f10,plain,
? [X0,X1,X2] :
( mult(X0,ld(X1,mult(X1,X2))) != mult(X0,X2)
| mult(X0,X2) != mult(rd(mult(X0,X1),X1),X2) ),
inference(ennf_transformation,[],[f9]) ).
fof(f11,plain,
( mult(sK0,ld(sK1,mult(sK1,sK2))) != mult(sK0,sK2)
| mult(sK0,sK2) != mult(rd(mult(sK0,sK1),sK1),sK2) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2]),skolemize(X0,sK0),skolemize(X1,sK1),skolemize(X2,sK2)],[f10]) ).
fof(f12,plain,
! [X0] : ld(X0,mult(X0,X0)) = X0,
inference(cnf_transformation,[],[f1]) ).
fof(f13,plain,
! [X0] : rd(mult(X0,X0),X0) = X0,
inference(cnf_transformation,[],[f2]) ).
fof(f14,plain,
! [X0,X1] : mult(X1,ld(X1,X0)) = ld(X1,mult(X1,X0)),
inference(cnf_transformation,[],[f3]) ).
fof(f15,plain,
! [X0,X1] : mult(rd(X1,X0),X0) = rd(mult(X1,X0),X0),
inference(cnf_transformation,[],[f4]) ).
fof(f16,plain,
! [X2,X3,X0,X1] : ld(ld(X3,X2),mult(ld(X3,X2),mult(X1,X0))) = mult(ld(X3,mult(X3,X1)),X0),
inference(cnf_transformation,[],[f5]) ).
fof(f17,plain,
! [X2,X3,X0,X1] : rd(mult(mult(X3,X2),rd(X1,X0)),rd(X1,X0)) = mult(X3,rd(mult(X2,X0),X0)),
inference(cnf_transformation,[],[f6]) ).
fof(f18,plain,
! [X0,X1] : ld(X1,mult(X1,ld(X0,X0))) = rd(mult(rd(X1,X1),X0),X0),
inference(cnf_transformation,[],[f7]) ).
fof(f19,plain,
( mult(sK0,ld(sK1,mult(sK1,sK2))) != mult(sK0,sK2)
| mult(sK0,sK2) != mult(rd(mult(sK0,sK1),sK1),sK2) ),
inference(cnf_transformation,[],[f11]) ).
fof(f21,definition,
( spl3_1
<=> mult(sK0,sK2) = mult(rd(mult(sK0,sK1),sK1),sK2) ),
introduced(definition,[new_symbols(definition,[spl3_1])],[avatar_definition]) ).
fof(f23,plain,
( mult(sK0,sK2) != mult(rd(mult(sK0,sK1),sK1),sK2)
| spl3_1 ),
inference(avatar_component_clause,[],[f21]) ).
fof(f25,definition,
( spl3_2
<=> mult(sK0,ld(sK1,mult(sK1,sK2))) = mult(sK0,sK2) ),
introduced(definition,[new_symbols(definition,[spl3_2])],[avatar_definition]) ).
fof(f27,plain,
( mult(sK0,ld(sK1,mult(sK1,sK2))) != mult(sK0,sK2)
| spl3_2 ),
inference(avatar_component_clause,[],[f25]) ).
fof(f28,plain,
( ~ spl3_1
| ~ spl3_2 ),
inference(avatar_split_clause,[],[f19,f25,f21]) ).
fof(f29,plain,
! [X0] : mult(X0,ld(X0,X0)) = X0,
inference(superposition,[],[f14,f12]) ).
fof(f31,plain,
! [X0] : ld(X0,X0) = mult(X0,ld(X0,ld(X0,X0))),
inference(superposition,[],[f14,f29]) ).
fof(f33,plain,
! [X0] : mult(rd(X0,X0),X0) = X0,
inference(superposition,[],[f15,f13]) ).
fof(f34,plain,
( mult(sK0,sK2) != mult(mult(rd(sK0,sK1),sK1),sK2)
| spl3_1 ),
inference(superposition,[],[f23,f15]) ).
fof(f36,plain,
! [X0] : rd(X0,X0) = mult(rd(rd(X0,X0),X0),X0),
inference(superposition,[],[f15,f33]) ).
fof(f42,plain,
! [X0,X1] : ld(X1,mult(X1,ld(X0,X0))) = mult(rd(rd(X1,X1),X0),X0),
inference(forward_demodulation,[],[f18,f15]) ).
fof(f43,plain,
! [X0,X1] : mult(rd(rd(X1,X1),X0),X0) = mult(X1,ld(X1,ld(X0,X0))),
inference(forward_demodulation,[],[f42,f14]) ).
fof(f45,plain,
! [X0] : rd(X0,X0) = mult(X0,ld(X0,ld(rd(X0,X0),rd(X0,X0)))),
inference(superposition,[],[f43,f33]) ).
fof(f46,plain,
! [X0] : rd(X0,X0) = mult(X0,ld(X0,ld(X0,X0))),
inference(superposition,[],[f36,f43]) ).
fof(f50,plain,
! [X0] : ld(X0,X0) = rd(X0,X0),
inference(forward_demodulation,[],[f46,f31]) ).
fof(f52,plain,
! [X0,X1] : mult(X0,ld(X0,ld(X1,X1))) = mult(rd(ld(X0,X0),X1),X1),
inference(superposition,[],[f43,f50]) ).
fof(f54,plain,
! [X0] : mult(ld(X0,X0),X0) = X0,
inference(superposition,[],[f33,f50]) ).
fof(f69,plain,
! [X0] : ld(X0,X0) = mult(X0,ld(X0,ld(ld(X0,X0),ld(X0,X0)))),
inference(forward_demodulation,[],[f45,f50]) ).
fof(f91,plain,
! [X2,X3,X0,X1] : ld(ld(X3,X2),mult(ld(X3,X2),mult(X1,X0))) = mult(mult(X3,ld(X3,X1)),X0),
inference(forward_demodulation,[],[f16,f14]) ).
fof(f92,plain,
! [X2,X3,X0,X1] : mult(mult(X3,ld(X3,X1)),X0) = mult(ld(X3,X2),ld(ld(X3,X2),mult(X1,X0))),
inference(forward_demodulation,[],[f91,f14]) ).
fof(f93,plain,
! [X2,X3,X0,X1] : rd(mult(mult(X3,X2),rd(X1,X0)),rd(X1,X0)) = mult(X3,mult(rd(X2,X0),X0)),
inference(forward_demodulation,[],[f17,f15]) ).
fof(f94,plain,
! [X2,X3,X0,X1] : mult(X3,mult(rd(X2,X0),X0)) = mult(rd(mult(X3,X2),rd(X1,X0)),rd(X1,X0)),
inference(forward_demodulation,[],[f93,f15]) ).
fof(f95,plain,
! [X2,X0,X1] : mult(mult(X0,ld(X0,X1)),X2) = mult(X0,ld(X0,mult(X1,X2))),
inference(superposition,[],[f92,f12]) ).
fof(f125,plain,
! [X0,X1] : mult(X0,X1) = mult(X0,ld(X0,mult(X0,X1))),
inference(superposition,[],[f95,f29]) ).
fof(f126,plain,
! [X0,X1] : mult(ld(X0,X0),X1) = mult(X0,ld(X0,mult(ld(X0,X0),X1))),
inference(superposition,[],[f95,f31]) ).
fof(f150,plain,
! [X0,X1] : mult(X0,X1) = mult(X0,mult(X0,ld(X0,X1))),
inference(forward_demodulation,[],[f125,f14]) ).
fof(f157,plain,
! [X0] : mult(X0,ld(X0,X0)) = mult(X0,ld(ld(X0,X0),ld(X0,X0))),
inference(superposition,[],[f150,f69]) ).
fof(f173,plain,
! [X0] : mult(X0,ld(ld(X0,X0),ld(X0,X0))) = X0,
inference(forward_demodulation,[],[f157,f29]) ).
fof(f212,plain,
! [X2,X0,X1] : mult(ld(X1,X2),ld(ld(X1,X2),X0)) = mult(mult(X1,ld(X1,X0)),ld(ld(X0,X0),ld(X0,X0))),
inference(superposition,[],[f92,f173]) ).
fof(f216,plain,
! [X2,X0,X1] : mult(ld(X1,X2),ld(ld(X1,X2),X0)) = mult(X1,ld(X1,mult(X0,ld(ld(X0,X0),ld(X0,X0))))),
inference(forward_demodulation,[],[f212,f95]) ).
fof(f217,plain,
! [X2,X0,X1] : mult(X1,ld(X1,X0)) = mult(ld(X1,X2),ld(ld(X1,X2),X0)),
inference(forward_demodulation,[],[f216,f173]) ).
fof(f252,plain,
! [X0] : ld(ld(X0,X0),ld(X0,X0)) = mult(X0,ld(X0,ld(ld(X0,X0),ld(X0,X0)))),
inference(superposition,[],[f126,f69]) ).
fof(f269,plain,
! [X0] : ld(X0,X0) = ld(ld(X0,X0),ld(X0,X0)),
inference(forward_demodulation,[],[f252,f69]) ).
fof(f326,plain,
! [X2,X0,X1] : mult(ld(X0,X1),mult(ld(X0,X1),ld(ld(X0,X1),X2))) = mult(X0,ld(X0,mult(ld(X0,X1),X2))),
inference(superposition,[],[f217,f14]) ).
fof(f332,plain,
! [X0,X1] : ld(X0,X1) = mult(X0,ld(X0,ld(X0,X1))),
inference(superposition,[],[f217,f29]) ).
fof(f362,plain,
! [X2,X0,X1] : mult(ld(X0,X1),X2) = mult(X0,ld(X0,mult(ld(X0,X1),X2))),
inference(forward_demodulation,[],[f326,f150]) ).
fof(f371,plain,
! [X2,X0,X1] : ld(ld(X0,X1),X2) = mult(X0,ld(X0,ld(ld(X0,X1),X2))),
inference(superposition,[],[f332,f217]) ).
fof(f505,plain,
! [X2,X0,X1] : mult(X0,mult(rd(ld(X0,X0),X1),X1)) = mult(rd(X0,rd(X2,X1)),rd(X2,X1)),
inference(superposition,[],[f94,f29]) ).
fof(f535,plain,
! [X2,X0,X1] : mult(X1,mult(rd(X2,X0),X0)) = mult(rd(mult(X1,X2),X0),X0),
inference(superposition,[],[f94,f13]) ).
fof(f563,plain,
! [X2,X0,X1] : mult(rd(X0,rd(X2,X1)),rd(X2,X1)) = mult(X0,mult(X0,ld(X0,ld(X1,X1)))),
inference(forward_demodulation,[],[f505,f52]) ).
fof(f572,plain,
! [X2,X0,X1] : mult(X0,ld(X1,X1)) = mult(rd(X0,rd(X2,X1)),rd(X2,X1)),
inference(forward_demodulation,[],[f563,f150]) ).
fof(f576,plain,
! [X0,X1] : mult(rd(X0,X1),X1) = mult(X0,mult(rd(ld(X0,X0),X1),X1)),
inference(superposition,[],[f535,f29]) ).
fof(f606,plain,
! [X0,X1] : mult(X0,mult(rd(X1,X1),X1)) = mult(mult(rd(X0,X1),X1),X1),
inference(superposition,[],[f535,f15]) ).
fof(f608,plain,
! [X0,X1] : mult(X0,X1) = mult(X0,mult(rd(X1,mult(X0,X1)),mult(X0,X1))),
inference(superposition,[],[f535,f33]) ).
fof(f621,plain,
! [X0,X1] : mult(X0,X1) = mult(mult(rd(X0,X1),X1),X1),
inference(forward_demodulation,[],[f606,f33]) ).
fof(f644,plain,
! [X0,X1] : mult(rd(X0,X1),X1) = mult(X0,mult(X0,ld(X0,ld(X1,X1)))),
inference(forward_demodulation,[],[f576,f52]) ).
fof(f658,plain,
! [X0,X1] : mult(X0,ld(X1,X1)) = mult(rd(X0,X1),X1),
inference(forward_demodulation,[],[f644,f150]) ).
fof(f663,plain,
! [X0,X1] : mult(rd(X0,X0),X1) = mult(mult(X0,ld(X0,ld(X1,X1))),X1),
inference(superposition,[],[f621,f43]) ).
fof(f679,plain,
! [X0,X1] : mult(rd(X0,X0),X1) = mult(X0,ld(X0,mult(ld(X1,X1),X1))),
inference(forward_demodulation,[],[f663,f95]) ).
fof(f683,plain,
! [X0,X1] : mult(rd(X0,X0),X1) = mult(X0,ld(X0,X1)),
inference(forward_demodulation,[],[f679,f54]) ).
fof(f684,plain,
! [X0,X1] : mult(X0,ld(X0,X1)) = mult(ld(X0,X0),X1),
inference(forward_demodulation,[],[f683,f50]) ).
fof(f686,plain,
! [X0,X1] : mult(mult(rd(X0,X1),X1),X1) = mult(mult(X0,X1),ld(X1,X1)),
inference(superposition,[],[f658,f15]) ).
fof(f703,plain,
! [X0,X1] : mult(X0,X1) = mult(mult(X0,ld(X1,X1)),X1),
inference(superposition,[],[f621,f658]) ).
fof(f704,plain,
! [X2,X0,X1] : mult(X0,mult(rd(X1,X2),X2)) = mult(mult(X0,X1),ld(X2,X2)),
inference(superposition,[],[f535,f658]) ).
fof(f707,plain,
( mult(sK0,sK2) != mult(mult(sK0,ld(sK1,sK1)),sK2)
| spl3_1 ),
inference(superposition,[],[f34,f658]) ).
fof(f719,plain,
! [X2,X0,X1] : mult(mult(X0,X1),ld(X2,X2)) = mult(X0,mult(X1,ld(X2,X2))),
inference(forward_demodulation,[],[f704,f658]) ).
fof(f728,plain,
! [X0,X1] : mult(X0,X1) = mult(mult(X0,X1),ld(X1,X1)),
inference(forward_demodulation,[],[f686,f621]) ).
fof(f793,plain,
! [X0,X1] : mult(rd(ld(X0,X0),X1),X1) = rd(mult(X0,ld(X0,X1)),X1),
inference(superposition,[],[f15,f684]) ).
fof(f795,plain,
! [X0,X1] : mult(ld(X0,X0),X1) = mult(X0,ld(X0,mult(ld(X0,X0),ld(ld(X0,X0),X1)))),
inference(superposition,[],[f150,f684]) ).
fof(f823,plain,
! [X0,X1] : mult(ld(X0,X0),X1) = mult(ld(X0,X0),ld(ld(X0,X0),X1)),
inference(forward_demodulation,[],[f795,f126]) ).
fof(f825,plain,
! [X0,X1] : mult(ld(X0,X0),ld(X1,X1)) = rd(mult(X0,ld(X0,X1)),X1),
inference(forward_demodulation,[],[f793,f658]) ).
fof(f863,plain,
! [X0,X1] : mult(ld(X0,X0),X1) = mult(X0,ld(X0,ld(ld(X0,X0),X1))),
inference(forward_demodulation,[],[f823,f684]) ).
fof(f865,plain,
! [X0,X1] : mult(X0,ld(X0,ld(X1,X1))) = rd(mult(X0,ld(X0,X1)),X1),
inference(forward_demodulation,[],[f825,f684]) ).
fof(f890,plain,
! [X0,X1] : mult(ld(X0,X0),X1) = ld(ld(X0,X0),X1),
inference(forward_demodulation,[],[f863,f371]) ).
fof(f905,plain,
! [X0,X1] : mult(X0,ld(X0,X1)) = ld(ld(X0,X0),X1),
inference(forward_demodulation,[],[f890,f684]) ).
fof(f1066,plain,
! [X0,X1] : rd(mult(X0,X1),ld(X1,X1)) = mult(rd(mult(X0,X1),ld(X1,X1)),ld(X1,X1)),
inference(superposition,[],[f15,f728]) ).
fof(f1068,plain,
! [X0,X1] : mult(mult(X0,X1),ld(ld(X1,X1),ld(X1,X1))) = rd(mult(X0,X1),ld(X1,X1)),
inference(forward_demodulation,[],[f1066,f658]) ).
fof(f1089,plain,
! [X0,X1] : mult(mult(X0,X1),ld(X1,X1)) = rd(mult(X0,X1),ld(X1,X1)),
inference(forward_demodulation,[],[f1068,f269]) ).
fof(f1097,plain,
! [X0,X1] : mult(X0,X1) = rd(mult(X0,X1),ld(X1,X1)),
inference(forward_demodulation,[],[f1089,f728]) ).
fof(f1543,plain,
! [X2,X0,X1] : mult(X0,ld(X1,X1)) = mult(X0,ld(rd(X2,X1),rd(X2,X1))),
inference(forward_demodulation,[],[f572,f658]) ).
fof(f1544,plain,
! [X0,X1] : mult(X0,X1) = mult(X0,mult(X1,ld(mult(X0,X1),mult(X0,X1)))),
inference(forward_demodulation,[],[f608,f658]) ).
fof(f1552,plain,
! [X2,X0,X1] : mult(X2,ld(ld(X1,X1),ld(X1,X1))) = mult(X2,ld(mult(X0,X1),mult(X0,X1))),
inference(superposition,[],[f1543,f1097]) ).
fof(f1578,plain,
! [X2,X0,X1] : mult(X0,rd(X2,X1)) = mult(mult(X0,ld(X1,X1)),rd(X2,X1)),
inference(superposition,[],[f703,f1543]) ).
fof(f1663,plain,
! [X2,X0,X1] : mult(X2,ld(X1,X1)) = mult(X2,ld(mult(X0,X1),mult(X0,X1))),
inference(forward_demodulation,[],[f1552,f269]) ).
fof(f2523,plain,
! [X0,X1] : mult(mult(X0,ld(X0,ld(X1,X1))),X1) = mult(X0,mult(rd(ld(X0,X1),X1),X1)),
inference(superposition,[],[f535,f865]) ).
fof(f2541,plain,
! [X0,X1] : mult(mult(X0,ld(X0,ld(X1,X1))),X1) = mult(X0,mult(ld(X0,X1),ld(X1,X1))),
inference(forward_demodulation,[],[f2523,f658]) ).
fof(f2573,plain,
! [X0,X1] : mult(X0,ld(X0,mult(ld(X1,X1),X1))) = mult(X0,mult(ld(X0,X1),ld(X1,X1))),
inference(forward_demodulation,[],[f2541,f95]) ).
fof(f2590,plain,
! [X0,X1] : mult(X0,ld(X0,X1)) = mult(X0,mult(ld(X0,X1),ld(X1,X1))),
inference(forward_demodulation,[],[f2573,f54]) ).
fof(f2727,plain,
! [X2,X0,X1] : mult(X2,mult(X0,X1)) = mult(mult(X2,ld(ld(X1,X1),ld(X1,X1))),mult(X0,X1)),
inference(superposition,[],[f1578,f1097]) ).
fof(f2760,plain,
! [X2,X0,X1] : mult(X2,mult(X0,X1)) = mult(mult(X2,ld(X1,X1)),mult(X0,X1)),
inference(forward_demodulation,[],[f2727,f269]) ).
fof(f3278,plain,
! [X2,X0,X1] : mult(X2,ld(X1,X1)) = mult(X2,ld(mult(X0,ld(X0,X1)),mult(X0,ld(X0,X1)))),
inference(superposition,[],[f1663,f684]) ).
fof(f3445,plain,
! [X2,X0,X1] : mult(X2,ld(X1,X1)) = mult(X2,ld(ld(X0,X1),ld(X0,X1))),
inference(forward_demodulation,[],[f3278,f1663]) ).
fof(f3712,plain,
! [X0,X1] : ld(X0,mult(X0,ld(X0,X1))) = mult(X0,ld(X0,mult(ld(X0,X1),ld(X1,X1)))),
inference(superposition,[],[f14,f2590]) ).
fof(f3740,plain,
! [X0,X1] : ld(X0,mult(X0,ld(X0,X1))) = mult(ld(X0,X1),ld(X1,X1)),
inference(forward_demodulation,[],[f3712,f362]) ).
fof(f3758,plain,
! [X0,X1] : mult(X0,ld(X0,ld(X0,X1))) = mult(ld(X0,X1),ld(X1,X1)),
inference(forward_demodulation,[],[f3740,f14]) ).
fof(f3770,plain,
! [X0,X1] : ld(X0,X1) = mult(ld(X0,X1),ld(X1,X1)),
inference(forward_demodulation,[],[f3758,f332]) ).
fof(f3815,plain,
! [X0,X1] : ld(ld(X0,X1),ld(X0,X1)) = mult(ld(X0,X1),ld(ld(X0,X1),ld(X1,X1))),
inference(superposition,[],[f14,f3770]) ).
fof(f3836,plain,
! [X0,X1] : mult(X0,ld(X0,ld(X1,X1))) = ld(ld(X0,X1),ld(X0,X1)),
inference(forward_demodulation,[],[f3815,f217]) ).
fof(f3912,plain,
! [X2,X0,X1] : mult(X2,ld(X0,X1)) = mult(mult(X2,ld(ld(X1,X1),ld(X1,X1))),ld(X0,X1)),
inference(superposition,[],[f2760,f3770]) ).
fof(f3967,plain,
! [X2,X0,X1] : mult(X2,ld(X0,X1)) = mult(mult(X2,ld(X1,X1)),ld(X0,X1)),
inference(forward_demodulation,[],[f3912,f269]) ).
fof(f4540,plain,
! [X2,X0,X1] : mult(X0,ld(X1,X1)) = mult(X0,mult(ld(ld(X2,X1),ld(X2,X1)),ld(mult(X0,ld(X1,X1)),mult(X0,ld(X1,X1))))),
inference(superposition,[],[f1544,f3445]) ).
fof(f4603,plain,
! [X2,X0,X1] : mult(X0,ld(X1,X1)) = mult(X0,mult(ld(ld(X2,X1),ld(X2,X1)),ld(ld(X1,X1),ld(X1,X1)))),
inference(forward_demodulation,[],[f4540,f1663]) ).
fof(f4664,plain,
! [X2,X0,X1] : mult(X0,ld(X1,X1)) = mult(X0,mult(ld(ld(X2,X1),ld(X2,X1)),ld(X1,X1))),
inference(forward_demodulation,[],[f4603,f3445]) ).
fof(f4710,plain,
! [X2,X0,X1] : mult(X0,ld(X1,X1)) = mult(X0,mult(ld(X2,X1),ld(ld(X2,X1),ld(X1,X1)))),
inference(forward_demodulation,[],[f4664,f684]) ).
fof(f4752,plain,
! [X2,X0,X1] : mult(X0,ld(X1,X1)) = mult(X0,mult(X2,ld(X2,ld(X1,X1)))),
inference(forward_demodulation,[],[f4710,f217]) ).
fof(f5734,plain,
! [X2,X0,X1] : mult(ld(X0,X1),ld(ld(X0,X1),X2)) = mult(mult(X0,ld(X0,ld(X1,X1))),X2),
inference(superposition,[],[f684,f3836]) ).
fof(f5740,plain,
! [X2,X0,X1] : mult(ld(X0,X1),ld(ld(X0,X1),X2)) = ld(mult(X0,ld(X0,ld(X1,X1))),X2),
inference(superposition,[],[f905,f3836]) ).
fof(f5795,plain,
! [X2,X0,X1] : mult(X0,ld(X0,X2)) = ld(mult(X0,ld(X0,ld(X1,X1))),X2),
inference(forward_demodulation,[],[f5740,f217]) ).
fof(f5796,plain,
! [X2,X0,X1] : mult(ld(X0,X1),ld(ld(X0,X1),X2)) = mult(X0,ld(X0,mult(ld(X1,X1),X2))),
inference(forward_demodulation,[],[f5734,f95]) ).
fof(f5832,plain,
! [X2,X0,X1] : mult(ld(X0,X1),ld(ld(X0,X1),X2)) = mult(X0,ld(X0,mult(X1,ld(X1,X2)))),
inference(forward_demodulation,[],[f5796,f684]) ).
fof(f5858,plain,
! [X2,X0,X1] : mult(X0,ld(X0,X2)) = mult(X0,ld(X0,mult(X1,ld(X1,X2)))),
inference(forward_demodulation,[],[f5832,f217]) ).
fof(f8549,plain,
! [X2,X0,X1] : mult(X0,mult(X0,ld(X0,X1))) = mult(X0,mult(X2,ld(X2,X1))),
inference(superposition,[],[f150,f5858]) ).
fof(f8564,plain,
! [X2,X0,X1] : ld(X0,mult(X0,ld(X0,X1))) = mult(X0,ld(X0,ld(X0,mult(X2,ld(X2,X1))))),
inference(superposition,[],[f14,f5858]) ).
fof(f8619,plain,
! [X2,X0,X1] : ld(X0,mult(X0,ld(X0,X1))) = ld(X0,mult(X2,ld(X2,X1))),
inference(forward_demodulation,[],[f8564,f332]) ).
fof(f8634,plain,
! [X2,X0,X1] : mult(X0,X1) = mult(X0,mult(X2,ld(X2,X1))),
inference(forward_demodulation,[],[f8549,f150]) ).
fof(f8679,plain,
! [X2,X0,X1] : mult(X0,ld(X0,ld(X0,X1))) = ld(X0,mult(X2,ld(X2,X1))),
inference(forward_demodulation,[],[f8619,f14]) ).
fof(f8721,plain,
! [X2,X0,X1] : ld(X0,X1) = ld(X0,mult(X2,ld(X2,X1))),
inference(forward_demodulation,[],[f8679,f332]) ).
fof(f9005,plain,
! [X2,X0,X1] : ld(X2,X1) = ld(X2,mult(X0,ld(mult(X0,ld(X1,X1)),X1))),
inference(superposition,[],[f8721,f3967]) ).
fof(f9006,plain,
! [X2,X3,X0,X1] : ld(X3,X2) = ld(X3,mult(X0,ld(X0,mult(X1,ld(mult(X0,ld(X0,X1)),X2))))),
inference(superposition,[],[f8721,f95]) ).
fof(f9185,plain,
! [X2,X3,X0,X1] : ld(X3,X2) = ld(X3,mult(X1,ld(mult(X0,ld(X0,X1)),X2))),
inference(forward_demodulation,[],[f9006,f8721]) ).
fof(f12538,plain,
! [X0,X1] : ld(X0,X1) = mult(X0,ld(X0,ld(mult(X0,ld(X1,X1)),X1))),
inference(superposition,[],[f9005,f14]) ).
fof(f14307,plain,
! [X2,X0,X1] : ld(X0,X2) = mult(X0,ld(X0,ld(mult(X1,ld(X1,X0)),X2))),
inference(superposition,[],[f9185,f14]) ).
fof(f17589,plain,
! [X2,X3,X0,X1] : mult(X2,ld(X0,X1)) = mult(X2,ld(mult(X3,ld(X3,X0)),X1)),
inference(superposition,[],[f8634,f14307]) ).
fof(f23796,plain,
! [X2,X0,X1] : ld(mult(X0,ld(X0,X1)),X2) = mult(ld(ld(mult(X0,ld(X0,X1)),X2),ld(mult(X0,ld(X0,X1)),X2)),ld(X1,X2)),
inference(superposition,[],[f54,f17589]) ).
fof(f23858,plain,
! [X2,X0,X1] : ld(mult(X0,ld(X0,X1)),X2) = mult(ld(mult(X0,ld(X0,X1)),X2),ld(ld(mult(X0,ld(X0,X1)),X2),ld(X1,X2))),
inference(forward_demodulation,[],[f23796,f684]) ).
fof(f24095,plain,
! [X2,X0,X1] : ld(mult(X0,ld(X0,X1)),X2) = mult(mult(X0,ld(X0,X1)),ld(mult(X0,ld(X0,X1)),ld(X1,X2))),
inference(forward_demodulation,[],[f23858,f217]) ).
fof(f24285,plain,
! [X2,X0,X1] : ld(mult(X0,ld(X0,X1)),X2) = mult(mult(X0,ld(X0,X1)),ld(X1,ld(X1,X2))),
inference(forward_demodulation,[],[f24095,f17589]) ).
fof(f24400,plain,
! [X2,X0,X1] : ld(mult(X0,ld(X0,X1)),X2) = mult(X0,ld(X0,mult(X1,ld(X1,ld(X1,X2))))),
inference(forward_demodulation,[],[f24285,f95]) ).
fof(f24469,plain,
! [X2,X0,X1] : mult(X0,ld(X0,ld(X1,X2))) = ld(mult(X0,ld(X0,X1)),X2),
inference(forward_demodulation,[],[f24400,f5858]) ).
fof(f26436,plain,
! [X2,X0,X1] : ld(mult(X0,mult(X0,ld(X0,X1))),X2) = mult(X0,ld(X0,ld(mult(X0,X1),X2))),
inference(superposition,[],[f24469,f14]) ).
fof(f26950,plain,
! [X2,X0,X1] : ld(mult(X0,X1),X2) = mult(X0,ld(X0,ld(mult(X0,X1),X2))),
inference(forward_demodulation,[],[f26436,f150]) ).
fof(f27696,plain,
! [X0,X1] : ld(X0,X1) = ld(mult(X0,ld(X1,X1)),X1),
inference(superposition,[],[f26950,f12538]) ).
fof(f27710,plain,
! [X2,X0,X1] : mult(X0,ld(X0,X2)) = ld(ld(mult(X0,X1),mult(X0,X1)),X2),
inference(superposition,[],[f5795,f26950]) ).
fof(f27786,plain,
! [X2,X0,X1] : mult(X0,ld(X0,X2)) = mult(mult(X0,X1),ld(mult(X0,X1),X2)),
inference(forward_demodulation,[],[f27710,f905]) ).
fof(f27912,plain,
! [X2,X0,X1] : ld(mult(X0,X1),X2) = ld(mult(X0,mult(X1,ld(X2,X2))),X2),
inference(superposition,[],[f27696,f719]) ).
fof(f31783,plain,
! [X2,X0,X1] : ld(mult(X2,ld(X0,X0)),X1) = ld(mult(X2,mult(X0,ld(X0,ld(X1,X1)))),X1),
inference(superposition,[],[f27912,f684]) ).
fof(f31980,plain,
! [X2,X0,X1] : ld(mult(X2,ld(X1,X1)),X1) = ld(mult(X2,ld(X0,X0)),X1),
inference(forward_demodulation,[],[f31783,f4752]) ).
fof(f32056,plain,
! [X2,X0,X1] : ld(X2,X1) = ld(mult(X2,ld(X0,X0)),X1),
inference(forward_demodulation,[],[f31980,f27696]) ).
fof(f32246,plain,
! [X2,X0,X1] : mult(X0,ld(X0,X1)) = mult(mult(X0,ld(X2,X2)),ld(X0,X1)),
inference(superposition,[],[f27786,f32056]) ).
fof(f37902,plain,
! [X2,X0,X1] : mult(X0,mult(X0,ld(X0,X1))) = mult(mult(X0,ld(X2,X2)),mult(X0,ld(X0,X1))),
inference(superposition,[],[f32246,f14]) ).
fof(f38093,plain,
! [X2,X0,X1] : mult(X0,mult(X0,ld(X0,X1))) = mult(mult(X0,ld(X2,X2)),X1),
inference(forward_demodulation,[],[f37902,f8634]) ).
fof(f38207,plain,
! [X2,X0,X1] : mult(X0,X1) = mult(mult(X0,ld(X2,X2)),X1),
inference(forward_demodulation,[],[f38093,f150]) ).
fof(f39468,plain,
( mult(sK0,sK2) != mult(sK0,sK2)
| spl3_1 ),
inference(superposition,[],[f707,f38207]) ).
fof(f39641,plain,
( $false
| spl3_1 ),
inference(trivial_inequality_removal,[],[f39468]) ).
fof(f39642,plain,
spl3_1,
inference(avatar_contradiction_clause,[],[f39641]) ).
fof(f40106,plain,
( mult(sK0,sK2) != mult(sK0,mult(sK1,ld(sK1,sK2)))
| spl3_2 ),
inference(forward_demodulation,[],[f27,f14]) ).
fof(f40108,plain,
( $false
| spl3_2 ),
inference(forward_subsumption_resolution,[],[f40106,f8634]) ).
fof(f40109,plain,
spl3_2,
inference(avatar_contradiction_clause,[],[f40108]) ).
cnf(s10,plain,
( ~ spl3_1
| ~ spl3_2 ),
inference(sat_conversion,[],[f28]) ).
cnf(s5545,plain,
spl3_1,
inference(sat_conversion,[],[f39642]) ).
cnf(s5568,plain,
spl3_2,
inference(sat_conversion,[],[f40109]) ).
cnf(s5569,plain,
$false,
inference(rat,[],[s10,s5568,s5545]) ).
fof(f40110,plain,
$false,
inference(avatar_sat_refutation,[],[s5569]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP683+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.11/0.38 % Computer : n017.cluster.edu
% 0.11/0.38 % Model : x86_64 x86_64
% 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38 % Memory : 8046.5625MB
% 0.11/0.38 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Sun Sep 27 10:31:20 UTC 2026
% 0.11/0.39 % CPUTime :
% 0.11/0.39 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.11/0.43 Running first-order model finding
% 0.11/0.43 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 6.18/1.42 % (2350435)Will run a generic schedule for satisfiability detection.
% 6.18/1.42 % (2350441)% WARNING: option uhcvi not known.
% 6.18/1.42 % (2350441)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=566499836:i=135531:add=off:rawr=on_3000 on theBenchmark for (3000ds/135531Mi)
% 6.18/1.42 % (2350443)dis+10_1_sil=32000:sp=arity:random_seed=1934885533:i=103:fgj=on_3000 on theBenchmark for (3000ds/103Mi)
% 6.18/1.42 % (2350442)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2951917300:i=88024:add=on:rawr=on_3000 on theBenchmark for (3000ds/88024Mi)
% 6.18/1.42 % (2350444)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2754786054:i=116_3000 on theBenchmark for (3000ds/116Mi)
% 6.18/1.42 % (2350446)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=4022568522:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_3000 on theBenchmark for (3000ds/159Mi)
% 6.18/1.42 % (2350445)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1000028315:i=131_3000 on theBenchmark for (3000ds/131Mi)
% 6.18/1.42 % (2350440)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1965998538_3000 on theBenchmark for (3000ds/0Mi)
% 6.18/1.42 % TRYING [1]
% 6.18/1.42 % TRYING [2]
% 6.18/1.42 % TRYING [3]
% 6.18/1.42 % TRYING [4]
% 6.18/1.42 % (2350443)Instruction limit reached!
% 6.18/1.42 % (2350443)------------------------------
% 6.18/1.42 % (2350443)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.18/1.42 % (2350443)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.18/1.42 % (2350443)CaDiCaL version: 2.1.3
% 6.18/1.42 % (2350443)Termination reason: Instruction limit
% 6.18/1.42 % (2350443)Termination phase: Saturation
% 6.18/1.42 % (2350443)Time elapsed: 0.099 s
% 6.18/1.42 % (2350443)Peak memory usage: 12 MB
% 6.18/1.42 % (2350443)Instructions burned: 104 (million)
% 6.18/1.42 % (2350444)Instruction limit reached!
% 6.18/1.42 % (2350444)------------------------------
% 6.18/1.42 % (2350444)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.18/1.42 % (2350444)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.18/1.42 % (2350444)CaDiCaL version: 2.1.3
% 6.18/1.42 % (2350444)Termination reason: Instruction limit
% 6.18/1.42 % (2350444)Termination phase: Saturation
% 6.18/1.42 % (2350444)Time elapsed: 0.114 s
% 6.18/1.42 % (2350444)Peak memory usage: 13 MB
% 6.18/1.42 % (2350444)Instructions burned: 116 (million)
% 6.18/1.42 % (2350445)Instruction limit reached!
% 6.18/1.42 % (2350445)------------------------------
% 6.18/1.42 % (2350445)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.18/1.42 % (2350445)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.18/1.42 % (2350445)CaDiCaL version: 2.1.3
% 6.18/1.42 % (2350445)Termination reason: Instruction limit
% 6.18/1.42 % (2350445)Termination phase: Saturation
% 6.18/1.42 % (2350445)Time elapsed: 0.129 s
% 6.18/1.42 % (2350445)Peak memory usage: 13 MB
% 6.18/1.42 % (2350445)Instructions burned: 132 (million)
% 6.18/1.42 % (2350456)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1574748145:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi)
% 6.18/1.42 % TRYING [1]
% 6.18/1.42 % TRYING [2]
% 6.18/1.42 % (2350458)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=609845293:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 6.18/1.42 % TRYING [3]
% 6.18/1.42 % (2350457)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3352569721:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 6.18/1.42 % TRYING [4]
% 6.18/1.42 % (2350446)Instruction limit reached!
% 6.18/1.42 % (2350446)------------------------------
% 6.18/1.42 % (2350446)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.18/1.42 % (2350446)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.18/1.42 % (2350446)CaDiCaL version: 2.1.3
% 6.18/1.42 % (2350446)Termination reason: Instruction limit
% 6.18/1.42 % (2350446)Termination phase: Saturation
% 6.18/1.42 % (2350446)Time elapsed: 0.166 s
% 6.18/1.42 % (2350446)Peak memory usage: 13 MB
% 6.18/1.42 % (2350446)Instructions burned: 160 (million)
% 6.18/1.42 % TRYING [5]
% 6.18/1.42 % (2350462)ott-21_1_sil=16000:fs=off:random_seed=1319512685:i=180:av=off:fsr=off_2997 on theBenchmark for (2997ds/180Mi)
% 6.18/1.42 % (2350457)Instruction limit reached!
% 6.18/1.42 % (2350457)------------------------------
% 6.18/1.42 % (2350457)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.18/1.42 % (2350457)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.18/1.42 % (2350457)CaDiCaL version: 2.1.3
% 6.18/1.42 % (2350457)Termination reason: Instruction limit
% 6.18/1.42 % (2350457)Termination phase: Saturation
% 6.18/1.42 % (2350457)Time elapsed: 0.139 s
% 6.18/1.42 % (2350457)Peak memory usage: 12 MB
% 6.18/1.42 % (2350457)Instructions burned: 131 (million)
% 6.18/1.42 % (2350464)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1575586375:i=477:bd=all_2996 on theBenchmark for (2996ds/477Mi)
% 6.18/1.42 % (2350462)Instruction limit reached!
% 6.18/1.42 % (2350462)------------------------------
% 6.18/1.42 % (2350462)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.18/1.42 % (2350462)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.18/1.42 % (2350462)CaDiCaL version: 2.1.3
% 6.18/1.42 % (2350462)Termination reason: Instruction limit
% 6.18/1.42 % (2350462)Termination phase: Saturation
% 6.18/1.42 % (2350462)Time elapsed: 0.157 s
% 6.18/1.42 % (2350462)Peak memory usage: 13 MB
% 6.18/1.42 % (2350462)Instructions burned: 180 (million)
% 6.18/1.42 % TRYING [5]
% 6.18/1.42 % (2350468)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=4090724403:fmbsr=1.3:i=865:ins=25_2996 on theBenchmark for (2996ds/865Mi)
% 6.18/1.42 % TRYING [1]
% 6.18/1.42 % TRYING [2]
% 6.18/1.42 % TRYING [3]
% 6.18/1.42 % TRYING [4]
% 6.18/1.42 % (2350458)Instruction limit reached!
% 6.18/1.42 % (2350458)------------------------------
% 6.18/1.42 % (2350458)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.18/1.42 % (2350458)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.18/1.42 % (2350458)CaDiCaL version: 2.1.3
% 6.18/1.42 % (2350458)Termination reason: Instruction limit
% 6.18/1.42 % (2350458)Termination phase: Saturation
% 6.18/1.42 % (2350458)Time elapsed: 0.317 s
% 6.18/1.42 % (2350458)Peak memory usage: 19 MB
% 6.18/1.42 % (2350458)Instructions burned: 685 (million)
% 6.18/1.42 % (2350473)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2564624890:i=1179_2995 on theBenchmark for (2995ds/1179Mi)
% 6.18/1.42 % TRYING [5]
% 6.18/1.42 % (2350464)Instruction limit reached!
% 6.18/1.42 % (2350464)------------------------------
% 6.18/1.42 % (2350464)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.18/1.42 % (2350464)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.18/1.42 % (2350464)CaDiCaL version: 2.1.3
% 6.18/1.42 % (2350464)Termination reason: Instruction limit
% 6.18/1.42 % (2350464)Termination phase: Saturation
% 6.18/1.42 % (2350464)Time elapsed: 0.313 s
% 6.18/1.42 % (2350464)Peak memory usage: 16 MB
% 6.18/1.42 % (2350464)Instructions burned: 479 (million)
% 6.18/1.42 % (2350503)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1698450259:i=889:ins=1_2993 on theBenchmark for (2993ds/889Mi)
% 6.18/1.42 % (2350456)Instruction limit reached!
% 6.18/1.42 % (2350456)------------------------------
% 6.18/1.42 % (2350456)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.18/1.42 % (2350456)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.18/1.42 % (2350456)CaDiCaL version: 2.1.3
% 6.18/1.42 % (2350456)Termination reason: Instruction limit
% 6.18/1.42 % (2350456)Termination phase: Finite model building SAT solving
% 6.18/1.42 % (2350456)Time elapsed: 0.523 s
% 6.18/1.42 % (2350456)Peak memory usage: 23 MB
% 6.18/1.42 % (2350456)Instructions burned: 715 (million)
% 6.18/1.42 % (2350516)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=3841645877:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2993 on theBenchmark for (2993ds/692Mi)
% 6.18/1.42 % TRYING [14]
% 6.18/1.42 % (2350468)Instruction limit reached!
% 6.18/1.42 % (2350468)------------------------------
% 6.18/1.42 % (2350468)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.18/1.42 % (2350468)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.18/1.42 % (2350468)CaDiCaL version: 2.1.3
% 6.18/1.42 % (2350468)Termination reason: Instruction limit
% 6.18/1.42 % (2350468)Termination phase: Finite model building SAT solving
% 6.18/1.42 % (2350468)Time elapsed: 0.443 s
% 6.18/1.42 % (2350468)Peak memory usage: 19 MB
% 6.18/1.42 % (2350468)Instructions burned: 866 (million)
% 6.18/1.42 % (2350473)Instruction limit reached!
% 6.18/1.42 % (2350473)------------------------------
% 6.18/1.42 % (2350473)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.18/1.42 % (2350473)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.18/1.42 % (2350473)CaDiCaL version: 2.1.3
% 6.18/1.42 % (2350473)Termination reason: Instruction limit
% 6.18/1.42 % (2350473)Termination phase: Saturation
% 6.18/1.42 % (2350473)Time elapsed: 0.378 s
% 6.18/1.42 % (2350473)Peak memory usage: 24 MB
% 6.18/1.42 % (2350473)Instructions burned: 1182 (million)
% 6.18/1.42 % (2350574)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1803914069:i=879:kws=inv_precedence:fsr=off_2991 on theBenchmark for (2991ds/879Mi)
% 6.18/1.42 % (2350581)fmb+10_1_sil=64000:random_seed=3576354649:i=22061:nm=2:gsp=on_2991 on theBenchmark for (2991ds/22061Mi)
% 6.18/1.42 % TRYING [1]
% 6.18/1.42 % TRYING [2]
% 6.18/1.42 % TRYING [3]
% 6.18/1.42 % TRYING [4]
% 6.18/1.42 % TRYING [5]
% 6.18/1.42 % (2350442) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-2350435-2350442"...
% 6.18/1.42 % (2350442)...printing done.
% 6.18/1.42 % (2350442)Refutation found. Thanks to Tanya!
% 6.18/1.42 % SZS status Theorem for theBenchmark
% 6.18/1.42 % SZS output start Proof for theBenchmark
% See solution above
% 6.18/1.43 % (2350442)------------------------------
% 6.18/1.43 % (2350442)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.18/1.43 % (2350442)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.18/1.43 % (2350442)CaDiCaL version: 2.1.3
% 6.18/1.43 % (2350442)Termination reason: Refutation
% 6.18/1.43 % (2350442)Time elapsed: 0.935 s
% 6.18/1.43 % (2350442)Peak memory usage: 25 MB
% 6.18/1.43 % (2350442)Instructions burned: 1369 (million)
% 6.18/1.43 % (2350435)Success in time 0.983 s
% 6.18/1.43 % Vampire exiting
%------------------------------------------------------------------------------