%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : LCL896+1 : TPTP v9.3.1. Released v5.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n005.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 12:00:57 PM UTC 2026
% Result : Theorem 4.25s 1.08s
% Output : Refutation 4.25s
% Verified :
% SZS Type : Refutation
% Derivation depth : 26
% Number of leaves : 17
% Syntax : Number of formulae : 121 ( 89 unt; 6 def)
% Number of atoms : 163 ( 64 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 82 ( 40 ~; 34 |; 2 &)
% ( 3 <=>; 3 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 2 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 5 ( 3 usr; 3 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 7 con; 0-2 aty)
% Number of variables : 102 ( 0 sgn 100 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1,X2] : '+'('+'(X0,X1),X2) = '+'(X0,'+'(X1,X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_01) ).
fof(f2,axiom,
! [X0,X1] : '+'(X0,X1) = '+'(X1,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_02) ).
fof(f3,axiom,
! [X0] : '+'(X0,'0') = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_03) ).
fof(f4,axiom,
! [X0] : '>='(X0,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_04) ).
fof(f6,axiom,
! [X0,X1] :
( ( '>='(X0,X1)
& '>='(X1,X0) )
=> X0 = X1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_06) ).
fof(f7,axiom,
! [X0,X1,X2] :
( '>='('+'(X0,X1),X2)
<=> '>='(X1,'==>'(X0,X2)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_07) ).
fof(f8,axiom,
! [X0] : '>='(X0,'0'),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_08) ).
fof(f9,axiom,
! [X0,X1,X2] :
( '>='(X0,X1)
=> '>='('+'(X0,X2),'+'(X1,X2)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_09) ).
fof(f11,axiom,
! [X0,X1,X2] :
( '>='(X0,X1)
=> '>='('==>'(X2,X0),'==>'(X2,X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_11) ).
fof(f12,axiom,
! [X0,X1,X2] : '+'('+'(X0,'==>'(X0,X1)),'==>'('+'(X0,'==>'(X0,X1)),X2)) = '+'(X0,'==>'(X0,'+'(X1,'==>'(X1,X2)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_12) ).
fof(f13,conjecture,
! [X0,X1] : '+'(X0,'==>'(X0,X1)) = '+'(X1,'==>'(X1,X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goals_13) ).
fof(f14,negated_conjecture,
~ ! [X0,X1] : '+'(X0,'==>'(X0,X1)) = '+'(X1,'==>'(X1,X0)),
inference(negated_conjecture,[status(cth)],[f13]) ).
fof(f17,plain,
! [X0,X1] :
( X0 = X1
| ~ '>='(X0,X1)
| ~ '>='(X1,X0) ),
inference(ennf_transformation,[],[f6]) ).
fof(f18,plain,
! [X0,X1] :
( X0 = X1
| ~ '>='(X0,X1)
| ~ '>='(X1,X0) ),
inference(flattening,[],[f17]) ).
fof(f19,plain,
! [X0,X1,X2] :
( '>='('+'(X0,X2),'+'(X1,X2))
| ~ '>='(X0,X1) ),
inference(ennf_transformation,[],[f9]) ).
fof(f21,plain,
! [X0,X1,X2] :
( '>='('==>'(X2,X0),'==>'(X2,X1))
| ~ '>='(X0,X1) ),
inference(ennf_transformation,[],[f11]) ).
fof(f22,plain,
? [X0,X1] : '+'(X0,'==>'(X0,X1)) != '+'(X1,'==>'(X1,X0)),
inference(ennf_transformation,[],[f14]) ).
fof(f23,plain,
! [X0,X1,X2] :
( ( '>='('+'(X0,X1),X2)
| ~ '>='(X1,'==>'(X0,X2)) )
& ( '>='(X1,'==>'(X0,X2))
| ~ '>='('+'(X0,X1),X2) ) ),
inference(nnf_transformation,[],[f7]) ).
fof(f24,plain,
'+'(sK0,'==>'(sK0,sK1)) != '+'(sK1,'==>'(sK1,sK0)),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1]),skolemize(X0,sK0),skolemize(X1,sK1)],[f22]) ).
fof(f25,plain,
! [X2,X0,X1] : '+'('+'(X0,X1),X2) = '+'(X0,'+'(X1,X2)),
inference(cnf_transformation,[],[f1]) ).
fof(f26,plain,
! [X0,X1] : '+'(X0,X1) = '+'(X1,X0),
inference(cnf_transformation,[],[f2]) ).
fof(f27,plain,
! [X0] : '+'(X0,'0') = X0,
inference(cnf_transformation,[],[f3]) ).
fof(f28,plain,
! [X0] : '>='(X0,X0),
inference(cnf_transformation,[],[f4]) ).
fof(f30,plain,
! [X0,X1] :
( ~ '>='(X1,X0)
| ~ '>='(X0,X1)
| X0 = X1 ),
inference(cnf_transformation,[],[f18]) ).
fof(f31,plain,
! [X2,X0,X1] :
( ~ '>='('+'(X0,X1),X2)
| '>='(X1,'==>'(X0,X2)) ),
inference(cnf_transformation,[],[f23]) ).
fof(f32,plain,
! [X2,X0,X1] :
( ~ '>='(X1,'==>'(X0,X2))
| '>='('+'(X0,X1),X2) ),
inference(cnf_transformation,[],[f23]) ).
fof(f33,plain,
! [X0] : '>='(X0,'0'),
inference(cnf_transformation,[],[f8]) ).
fof(f34,plain,
! [X2,X0,X1] :
( '>='('+'(X0,X2),'+'(X1,X2))
| ~ '>='(X0,X1) ),
inference(cnf_transformation,[],[f19]) ).
fof(f36,plain,
! [X2,X0,X1] :
( '>='('==>'(X2,X0),'==>'(X2,X1))
| ~ '>='(X0,X1) ),
inference(cnf_transformation,[],[f21]) ).
fof(f37,plain,
! [X2,X0,X1] : '+'('+'(X0,'==>'(X0,X1)),'==>'('+'(X0,'==>'(X0,X1)),X2)) = '+'(X0,'==>'(X0,'+'(X1,'==>'(X1,X2)))),
inference(cnf_transformation,[],[f12]) ).
fof(f38,plain,
'+'(sK0,'==>'(sK0,sK1)) != '+'(sK1,'==>'(sK1,sK0)),
inference(cnf_transformation,[],[f24]) ).
fof(f39,definition,
sF2 = '==>'(sK0,sK1),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f40,plain,
'==>'(sK0,sK1) = sF2,
inference(reorient_equations,[],[f39]) ).
fof(f41,definition,
sF3 = '+'(sK0,sF2),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f42,plain,
'+'(sK0,sF2) = sF3,
inference(reorient_equations,[],[f41]) ).
fof(f43,definition,
sF4 = '==>'(sK1,sK0),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f44,plain,
'==>'(sK1,sK0) = sF4,
inference(reorient_equations,[],[f43]) ).
fof(f45,definition,
sF5 = '+'(sK1,sF4),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f46,plain,
'+'(sK1,sF4) = sF5,
inference(reorient_equations,[],[f45]) ).
fof(f47,plain,
sF3 != sF5,
inference(definition_folding,[],[f38,f46,f44,f42,f40]) ).
fof(f48,plain,
sF3 = '+'(sF2,sK0),
inference(forward_demodulation,[],[f42,f26]) ).
fof(f49,plain,
sF5 = '+'(sF4,sK1),
inference(forward_demodulation,[],[f46,f26]) ).
fof(f53,plain,
! [X0] : '+'('0',X0) = X0,
inference(superposition,[],[f27,f26]) ).
fof(f61,plain,
! [X0] :
( ~ '>='('0',X0)
| '0' = X0 ),
inference(resolution,[],[f30,f33]) ).
fof(f64,plain,
! [X0,X1] : '>='(X0,'==>'(X1,'+'(X1,X0))),
inference(resolution,[],[f31,f28]) ).
fof(f66,plain,
! [X0,X1] :
( ~ '>='(X0,X1)
| '>='('0','==>'(X0,X1)) ),
inference(superposition,[],[f31,f27]) ).
fof(f79,plain,
! [X0,X1] : '>='('+'(X0,'==>'(X0,X1)),X1),
inference(resolution,[],[f32,f28]) ).
fof(f96,plain,
! [X0,X1] :
( '>='('+'(X1,X0),X0)
| ~ '>='(X1,'0') ),
inference(superposition,[],[f34,f53]) ).
fof(f99,plain,
! [X0,X1] : '>='('+'(X1,X0),X0),
inference(forward_subsumption_resolution,[],[f96,f33]) ).
fof(f110,plain,
'>='(sF3,sK0),
inference(superposition,[],[f99,f48]) ).
fof(f111,plain,
'>='(sF5,sK1),
inference(superposition,[],[f99,f49]) ).
fof(f132,plain,
! [X2,X0,X1] :
( ~ '>='('==>'(X2,X1),'==>'(X2,X0))
| ~ '>='(X0,X1)
| '==>'(X2,X0) = '==>'(X2,X1) ),
inference(resolution,[],[f36,f30]) ).
fof(f164,plain,
! [X2,X0,X1] : '+'(X0,'+'(X1,X2)) = '+'(X2,'+'(X0,X1)),
inference(superposition,[],[f26,f25]) ).
fof(f171,plain,
! [X0] : '+'(sK0,'==>'(sK0,'+'(sK1,'==>'(sK1,X0)))) = '+'('+'(sK0,sF2),'==>'('+'(sK0,sF2),X0)),
inference(superposition,[],[f37,f40]) ).
fof(f172,plain,
! [X0] : '+'(sK1,'==>'(sK1,'+'(sK0,'==>'(sK0,X0)))) = '+'('+'(sK1,sF4),'==>'('+'(sK1,sF4),X0)),
inference(superposition,[],[f37,f44]) ).
fof(f191,plain,
! [X0] : '+'(sK1,'==>'(sK1,'+'(sK0,'==>'(sK0,X0)))) = '+'(sK1,'+'(sF4,'==>'('+'(sK1,sF4),X0))),
inference(forward_demodulation,[],[f172,f25]) ).
fof(f192,plain,
! [X0] : '+'(sK0,'==>'(sK0,'+'(sK1,'==>'(sK1,X0)))) = '+'(sK0,'+'(sF2,'==>'('+'(sK0,sF2),X0))),
inference(forward_demodulation,[],[f171,f25]) ).
fof(f198,plain,
! [X0] : '+'(sK1,'==>'(sK1,'+'(sK0,'==>'(sK0,X0)))) = '+'(sK1,'+'(sF4,'==>'('+'(sF4,sK1),X0))),
inference(forward_demodulation,[],[f191,f26]) ).
fof(f199,plain,
! [X0] : '+'(sK0,'==>'(sK0,'+'(sK1,'==>'(sK1,X0)))) = '+'(sK0,'+'(sF2,'==>'('+'(sF2,sK0),X0))),
inference(forward_demodulation,[],[f192,f26]) ).
fof(f203,plain,
! [X0] : '+'(sK1,'==>'(sK1,'+'(sK0,'==>'(sK0,X0)))) = '+'(sK1,'+'(sF4,'==>'(sF5,X0))),
inference(forward_demodulation,[],[f198,f49]) ).
fof(f204,plain,
! [X0] : '+'(sK0,'==>'(sK0,'+'(sK1,'==>'(sK1,X0)))) = '+'(sK0,'+'(sF2,'==>'(sF3,X0))),
inference(forward_demodulation,[],[f199,f48]) ).
fof(f212,plain,
! [X0] : '0' = '==>'(X0,'+'(X0,'0')),
inference(resolution,[],[f64,f61]) ).
fof(f221,plain,
! [X0] : '0' = '==>'(X0,X0),
inference(forward_demodulation,[],[f212,f27]) ).
fof(f288,plain,
'>='('0','==>'(sF3,sK0)),
inference(resolution,[],[f66,f110]) ).
fof(f290,plain,
'>='('0','==>'(sF5,sK1)),
inference(resolution,[],[f66,f111]) ).
fof(f1489,plain,
! [X0,X1] :
( ~ '>='('+'(X0,'==>'(X0,X1)),X1)
| '==>'(X0,X1) = '==>'(X0,'+'(X0,'==>'(X0,X1))) ),
inference(resolution,[],[f132,f64]) ).
fof(f1502,plain,
! [X0,X1] : '==>'(X0,X1) = '==>'(X0,'+'(X0,'==>'(X0,X1))),
inference(forward_subsumption_resolution,[],[f1489,f79]) ).
fof(f1514,plain,
! [X0] : '>='('+'(sF4,'==>'(sF5,X0)),'==>'(sK1,'+'(sK1,'==>'(sK1,'+'(sK0,'==>'(sK0,X0)))))),
inference(superposition,[],[f64,f203]) ).
fof(f1538,plain,
! [X0] : '>='('+'(sF4,'==>'(sF5,X0)),'==>'(sK1,'+'(sK0,'==>'(sK0,X0)))),
inference(forward_demodulation,[],[f1514,f1502]) ).
fof(f1577,plain,
! [X0] : '>='('+'(sF2,'==>'(sF3,X0)),'==>'(sK0,'+'(sK0,'==>'(sK0,'+'(sK1,'==>'(sK1,X0)))))),
inference(superposition,[],[f64,f204]) ).
fof(f1601,plain,
! [X0] : '>='('+'(sF2,'==>'(sF3,X0)),'==>'(sK0,'+'(sK1,'==>'(sK1,X0)))),
inference(forward_demodulation,[],[f1577,f1502]) ).
fof(f2394,plain,
'0' = '==>'(sF3,sK0),
inference(resolution,[],[f288,f61]) ).
fof(f2709,plain,
'0' = '==>'(sF5,sK1),
inference(resolution,[],[f290,f61]) ).
fof(f4585,plain,
'+'(sK0,'+'(sF2,'0')) = '+'(sK0,'==>'(sK0,'+'(sK1,'==>'(sK1,sK0)))),
inference(superposition,[],[f204,f2394]) ).
fof(f4623,plain,
'+'(sK0,'+'(sF2,'0')) = '+'(sK0,'==>'(sK0,'+'(sK1,sF4))),
inference(forward_demodulation,[],[f4585,f44]) ).
fof(f4635,plain,
'+'(sK0,'+'(sF2,'0')) = '+'(sK0,'==>'(sK0,'+'(sF4,sK1))),
inference(forward_demodulation,[],[f4623,f26]) ).
fof(f4646,plain,
'+'(sK0,'==>'(sK0,sF5)) = '+'(sK0,'+'(sF2,'0')),
inference(forward_demodulation,[],[f4635,f49]) ).
fof(f4653,plain,
'+'(sK0,'==>'(sK0,sF5)) = '+'('0','+'(sK0,sF2)),
inference(forward_demodulation,[],[f4646,f164]) ).
fof(f4660,plain,
'+'(sK0,sF2) = '+'(sK0,'==>'(sK0,sF5)),
inference(forward_demodulation,[],[f4653,f53]) ).
fof(f4666,plain,
'+'(sF2,sK0) = '+'(sK0,'==>'(sK0,sF5)),
inference(forward_demodulation,[],[f4660,f26]) ).
fof(f4672,plain,
sF3 = '+'(sK0,'==>'(sK0,sF5)),
inference(forward_demodulation,[],[f4666,f48]) ).
fof(f4709,plain,
'+'(sK1,'+'(sF4,'0')) = '+'(sK1,'==>'(sK1,'+'(sK0,'==>'(sK0,sK1)))),
inference(superposition,[],[f203,f2709]) ).
fof(f4747,plain,
'+'(sK1,'+'(sF4,'0')) = '+'(sK1,'==>'(sK1,'+'(sK0,sF2))),
inference(forward_demodulation,[],[f4709,f40]) ).
fof(f4759,plain,
'+'(sK1,'+'(sF4,'0')) = '+'(sK1,'==>'(sK1,'+'(sF2,sK0))),
inference(forward_demodulation,[],[f4747,f26]) ).
fof(f4770,plain,
'+'(sK1,'+'(sF4,'0')) = '+'(sK1,'==>'(sK1,sF3)),
inference(forward_demodulation,[],[f4759,f48]) ).
fof(f4777,plain,
'+'('0','+'(sK1,sF4)) = '+'(sK1,'==>'(sK1,sF3)),
inference(forward_demodulation,[],[f4770,f164]) ).
fof(f4784,plain,
'+'(sK1,sF4) = '+'(sK1,'==>'(sK1,sF3)),
inference(forward_demodulation,[],[f4777,f53]) ).
fof(f4790,plain,
'+'(sF4,sK1) = '+'(sK1,'==>'(sK1,sF3)),
inference(forward_demodulation,[],[f4784,f26]) ).
fof(f4796,plain,
sF5 = '+'(sK1,'==>'(sK1,sF3)),
inference(forward_demodulation,[],[f4790,f49]) ).
fof(f12996,definition,
( spl6_96
<=> '>='(sF5,sF3) ),
introduced(definition,[new_symbols(definition,[spl6_96])],[avatar_definition]) ).
fof(f12997,plain,
( '>='(sF5,sF3)
| ~ spl6_96 ),
inference(avatar_component_clause,[],[f12996]) ).
fof(f12998,plain,
( ~ '>='(sF5,sF3)
| spl6_96 ),
inference(avatar_component_clause,[],[f12996]) ).
fof(f13098,definition,
( spl6_100
<=> '>='(sF3,sF5) ),
introduced(definition,[new_symbols(definition,[spl6_100])],[avatar_definition]) ).
fof(f13099,plain,
( '>='(sF3,sF5)
| ~ spl6_100 ),
inference(avatar_component_clause,[],[f13098]) ).
fof(f13100,plain,
( ~ '>='(sF3,sF5)
| spl6_100 ),
inference(avatar_component_clause,[],[f13098]) ).
fof(f26705,plain,
'>='('+'(sF4,'0'),'==>'(sK1,'+'(sK0,'==>'(sK0,sF5)))),
inference(superposition,[],[f1538,f221]) ).
fof(f26725,plain,
'>='('+'(sF4,'0'),'==>'(sK1,sF3)),
inference(forward_demodulation,[],[f26705,f4672]) ).
fof(f26745,plain,
'>='(sF4,'==>'(sK1,sF3)),
inference(forward_demodulation,[],[f26725,f27]) ).
fof(f26776,plain,
'>='('+'(sK1,sF4),sF3),
inference(resolution,[],[f26745,f32]) ).
fof(f26819,plain,
'>='('+'(sF4,sK1),sF3),
inference(forward_demodulation,[],[f26776,f26]) ).
fof(f26824,plain,
'>='(sF5,sF3),
inference(forward_demodulation,[],[f26819,f49]) ).
fof(f26828,plain,
( $false
| spl6_96 ),
inference(forward_subsumption_resolution,[],[f26824,f12998]) ).
fof(f26829,plain,
spl6_96,
inference(avatar_contradiction_clause,[],[f26828]) ).
fof(f26860,plain,
'>='('+'(sF2,'0'),'==>'(sK0,'+'(sK1,'==>'(sK1,sF3)))),
inference(superposition,[],[f1601,f221]) ).
fof(f26880,plain,
'>='('+'(sF2,'0'),'==>'(sK0,sF5)),
inference(forward_demodulation,[],[f26860,f4796]) ).
fof(f26900,plain,
'>='(sF2,'==>'(sK0,sF5)),
inference(forward_demodulation,[],[f26880,f27]) ).
fof(f26928,plain,
( ~ '>='(sF3,sF5)
| sF3 = sF5
| ~ spl6_96 ),
inference(resolution,[],[f12997,f30]) ).
fof(f27038,plain,
'>='('+'(sK0,sF2),sF5),
inference(resolution,[],[f26900,f32]) ).
fof(f27081,plain,
'>='('+'(sF2,sK0),sF5),
inference(forward_demodulation,[],[f27038,f26]) ).
fof(f27086,plain,
'>='(sF3,sF5),
inference(forward_demodulation,[],[f27081,f48]) ).
fof(f27090,plain,
( $false
| spl6_100 ),
inference(forward_subsumption_resolution,[],[f27086,f13100]) ).
fof(f27091,plain,
spl6_100,
inference(avatar_contradiction_clause,[],[f27090]) ).
fof(f27096,plain,
( sF3 = sF5
| ~ spl6_96
| ~ spl6_100 ),
inference(forward_subsumption_resolution,[],[f26928,f13099]) ).
fof(f27099,plain,
( $false
| ~ spl6_96
| ~ spl6_100 ),
inference(forward_subsumption_resolution,[],[f27096,f47]) ).
fof(f27100,plain,
( ~ spl6_96
| ~ spl6_100 ),
inference(avatar_contradiction_clause,[],[f27099]) ).
cnf(s87,plain,
spl6_96,
inference(sat_conversion,[],[f26829]) ).
cnf(s93,plain,
spl6_100,
inference(sat_conversion,[],[f27091]) ).
cnf(s94,plain,
( ~ spl6_96
| ~ spl6_100 ),
inference(sat_conversion,[],[f27100]) ).
cnf(s95,plain,
~ spl6_96,
inference(rat,[],[s94,s93]) ).
cnf(s96,plain,
$false,
inference(rat,[],[s87,s95]) ).
fof(f27107,plain,
$false,
inference(avatar_sat_refutation,[],[s96]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL896+1 : TPTP v9.3.1. Released v5.5.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.12/0.38 % Computer : n005.cluster.edu
% 0.12/0.38 % Model : x86_64 x86_64
% 0.12/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.38 % Memory : 8046.5625MB
% 0.12/0.38 % OS : Linux 6.8.0-71-generic
% 0.12/0.38 % CPULimit : 300
% 0.12/0.38 % WCLimit : 300
% 0.12/0.38 % DateTime : Sun Sep 27 17:05:02 UTC 2026
% 0.12/0.39 % CPUTime :
% 0.12/0.39 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.12/0.42 Running first-order model finding
% 0.12/0.42 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
% 4.25/1.08 % (19750)Will run a generic schedule for satisfiability detection.
% 4.25/1.08 % (19761)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2227795209:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 4.25/1.08 % (19756)% WARNING: option uhcvi not known.
% 4.25/1.08 % (19757)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=788000963:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 4.25/1.08 % (19759)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3314937461:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 4.25/1.08 % (19755)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2786328454_2999 on theBenchmark for (2999ds/0Mi)
% 4.25/1.08 % (19756)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3704708809:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 4.25/1.08 % (19758)dis+10_1_sil=32000:sp=arity:random_seed=3627605066:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 4.25/1.08 % (19760)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=856331990:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 4.25/1.08 % TRYING [1]
% 4.25/1.08 % TRYING [2]
% 4.25/1.08 % TRYING [3]
% 4.25/1.08 % TRYING [4]
% 4.25/1.08 % TRYING [5]
% 4.25/1.08 % (19761)Instruction limit reached!
% 4.25/1.08 % (19761)------------------------------
% 4.25/1.08 % (19761)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.25/1.08 % (19761)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.25/1.08 % (19761)CaDiCaL version: 2.1.3
% 4.25/1.08 % (19761)Termination reason: Instruction limit
% 4.25/1.08 % (19761)Termination phase: Saturation
% 4.25/1.08 % (19761)Time elapsed: 0.059 s
% 4.25/1.08 % (19761)Peak memory usage: 13 MB
% 4.25/1.08 % (19761)Instructions burned: 159 (million)
% 4.25/1.08 % (19758)Instruction limit reached!
% 4.25/1.08 % (19758)------------------------------
% 4.25/1.08 % (19758)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.25/1.08 % (19758)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.25/1.08 % (19758)CaDiCaL version: 2.1.3
% 4.25/1.08 % (19758)Termination reason: Instruction limit
% 4.25/1.08 % (19758)Termination phase: Saturation
% 4.25/1.08 % (19758)Time elapsed: 0.061 s
% 4.25/1.08 % (19758)Peak memory usage: 12 MB
% 4.25/1.08 % (19758)Instructions burned: 103 (million)
% 4.25/1.08 % (19769)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=511871489:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 4.25/1.08 % TRYING [1]
% 4.25/1.08 % TRYING [2]
% 4.25/1.08 % TRYING [3]
% 4.25/1.08 % (19759)Instruction limit reached!
% 4.25/1.08 % (19759)------------------------------
% 4.25/1.08 % (19759)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.25/1.08 % (19759)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.25/1.08 % (19759)CaDiCaL version: 2.1.3
% 4.25/1.08 % (19759)Termination reason: Instruction limit
% 4.25/1.08 % (19759)Termination phase: Saturation
% 4.25/1.08 % (19759)Time elapsed: 0.067 s
% 4.25/1.08 % (19759)Peak memory usage: 12 MB
% 4.25/1.08 % (19759)Instructions burned: 117 (million)
% 4.25/1.08 % TRYING [4]
% 4.25/1.08 % TRYING [5]
% 4.25/1.08 % (19770)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1915413731:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 4.25/1.08 % (19760)Instruction limit reached!
% 4.25/1.08 % (19760)------------------------------
% 4.25/1.08 % (19760)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.25/1.08 % (19760)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.25/1.08 % (19760)CaDiCaL version: 2.1.3
% 4.25/1.08 % (19760)Termination reason: Instruction limit
% 4.25/1.08 % (19760)Termination phase: Saturation
% 4.25/1.08 % (19760)Time elapsed: 0.080 s
% 4.25/1.08 % (19760)Peak memory usage: 13 MB
% 4.25/1.08 % (19760)Instructions burned: 131 (million)
% 4.25/1.08 % TRYING [6]
% 4.25/1.08 % (19772)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=667589769:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 4.25/1.08 % (19774)ott-21_1_sil=16000:fs=off:random_seed=3717494852:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 4.25/1.08 % TRYING [6]
% 4.25/1.08 % (19770)Instruction limit reached!
% 4.25/1.08 % (19770)------------------------------
% 4.25/1.08 % (19770)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.25/1.08 % (19770)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.25/1.08 % (19770)CaDiCaL version: 2.1.3
% 4.25/1.08 % (19770)Termination reason: Instruction limit
% 4.25/1.08 % (19770)Termination phase: Saturation
% 4.25/1.08 % (19770)Time elapsed: 0.084 s
% 4.25/1.08 % (19770)Peak memory usage: 13 MB
% 4.25/1.08 % (19770)Instructions burned: 131 (million)
% 4.25/1.08 % (19774)Instruction limit reached!
% 4.25/1.08 % (19774)------------------------------
% 4.25/1.08 % (19774)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.25/1.08 % (19774)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.25/1.08 % (19774)CaDiCaL version: 2.1.3
% 4.25/1.08 % (19774)Termination reason: Instruction limit
% 4.25/1.08 % (19774)Termination phase: Saturation
% 4.25/1.08 % (19774)Time elapsed: 0.074 s
% 4.25/1.08 % (19774)Peak memory usage: 12 MB
% 4.25/1.08 % (19774)Instructions burned: 180 (million)
% 4.25/1.08 % (19777)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2313916162:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 4.25/1.08 % TRYING [7]
% 4.25/1.08 % (19778)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=958947522:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 4.25/1.08 % TRYING [1]
% 4.25/1.08 % TRYING [2]
% 4.25/1.08 % TRYING [3]
% 4.25/1.08 % TRYING [4]
% 4.25/1.08 % (19769)Instruction limit reached!
% 4.25/1.08 % (19769)------------------------------
% 4.25/1.08 % (19769)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.25/1.08 % (19769)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.25/1.08 % (19769)CaDiCaL version: 2.1.3
% 4.25/1.08 % (19769)Termination reason: Instruction limit
% 4.25/1.08 % (19769)Termination phase: Finite model building constraint generation
% 4.25/1.08 % (19769)Time elapsed: 0.161 s
% 4.25/1.08 % (19769)Peak memory usage: 27 MB
% 4.25/1.08 % (19769)Instructions burned: 714 (million)
% 4.25/1.08 % (19781)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2726175386:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 4.25/1.08 % TRYING [5]
% 4.25/1.08 % TRYING [6]
% 4.25/1.08 % TRYING [7]
% 4.25/1.08 % (19772)Instruction limit reached!
% 4.25/1.08 % (19772)------------------------------
% 4.25/1.08 % (19772)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.25/1.08 % (19772)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.25/1.08 % (19772)CaDiCaL version: 2.1.3
% 4.25/1.08 % (19772)Termination reason: Instruction limit
% 4.25/1.08 % (19772)Termination phase: Saturation
% 4.25/1.08 % (19772)Time elapsed: 0.369 s
% 4.25/1.08 % (19772)Peak memory usage: 18 MB
% 4.25/1.08 % (19772)Instructions burned: 685 (million)
% 4.25/1.08 % (19783)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3707316305:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 4.25/1.08 % (19777)Instruction limit reached!
% 4.25/1.08 % (19777)------------------------------
% 4.25/1.08 % (19777)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.25/1.08 % (19777)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.25/1.08 % (19777)CaDiCaL version: 2.1.3
% 4.25/1.08 % (19777)Termination reason: Instruction limit
% 4.25/1.08 % (19777)Termination phase: Saturation
% 4.25/1.08 % (19777)Time elapsed: 0.290 s
% 4.25/1.08 % (19777)Peak memory usage: 14 MB
% 4.25/1.08 % (19777)Instructions burned: 478 (million)
% 4.25/1.08 % (19785)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=3917647807:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2994 on theBenchmark for (2994ds/692Mi)
% 4.25/1.08 % (19778)Instruction limit reached!
% 4.25/1.08 % (19778)------------------------------
% 4.25/1.08 % (19778)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.25/1.08 % (19778)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.25/1.08 % (19778)CaDiCaL version: 2.1.3
% 4.25/1.08 % (19778)Termination reason: Instruction limit
% 4.25/1.08 % (19778)Termination phase: Finite model building SAT solving
% 4.25/1.08 % (19778)Time elapsed: 0.330 s
% 4.25/1.08 % (19778)Peak memory usage: 22 MB
% 4.25/1.08 % (19778)Instructions burned: 867 (million)
% 4.25/1.08 % (19787)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1824996923:i=879:kws=inv_precedence:fsr=off_2994 on theBenchmark for (2994ds/879Mi)
% 4.25/1.08 % TRYING [14]
% 4.25/1.08 % (19781) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-19750-19781"...
% 4.25/1.08 % (19781)...printing done.
% 4.25/1.08 % (19781)Refutation found. Thanks to Tanya!
% 4.25/1.08 % SZS status Theorem for theBenchmark
% 4.25/1.08 % SZS output start Proof for theBenchmark
% See solution above
% 4.25/1.08 % (19781)------------------------------
% 4.25/1.08 % (19781)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.25/1.08 % (19781)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.25/1.08 % (19781)CaDiCaL version: 2.1.3
% 4.25/1.08 % (19781)Termination reason: Refutation
% 4.25/1.08 % (19781)Time elapsed: 0.377 s
% 4.25/1.08 % (19781)Peak memory usage: 24 MB
% 4.25/1.08 % (19781)Instructions burned: 1165 (million)
% 4.25/1.08 % (19750)Success in time 0.654 s
% 4.25/1.08 % Vampire exiting
%------------------------------------------------------------------------------