%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : LCL900+1 : TPTP v9.3.1. Released v5.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n012.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 198.17s 33.15s
% Output : Refutation 198.17s
% Verified :
% SZS Type : Refutation
% Derivation depth : 30
% Number of leaves : 14
% Syntax : Number of formulae : 124 ( 87 unt; 0 def)
% Number of atoms : 171 ( 66 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 90 ( 43 ~; 38 |; 3 &)
% ( 1 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 4 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 6 ( 6 usr; 4 con; 0-2 aty)
% Number of variables : 264 ( 262 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1,X2] : '+'('+'(X0,X1),X2) = '+'(X0,'+'(X1,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_01) ).
fof(f2,axiom,
! [X0,X1] : '+'(X0,X1) = '+'(X1,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_02) ).
fof(f3,axiom,
! [X0] : '+'(X0,'0') = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_03) ).
fof(f4,axiom,
! [X0] : '>='(X0,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_04) ).
fof(f5,axiom,
! [X0,X1,X2] :
( ( '>='(X0,X1)
& '>='(X1,X2) )
=> '>='(X0,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_05) ).
fof(f6,axiom,
! [X0,X1] :
( ( '>='(X0,X1)
& '>='(X1,X0) )
=> X0 = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_06) ).
fof(f7,axiom,
! [X0,X1,X2] :
( '>='('+'(X0,X1),X2)
<=> '>='(X1,'==>'(X0,X2)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_07) ).
fof(f8,axiom,
! [X0] : '>='(X0,'0'),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_08) ).
fof(f9,axiom,
! [X0,X1,X2] :
( '>='(X0,X1)
=> '>='('+'(X0,X2),'+'(X1,X2)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_09) ).
fof(f10,axiom,
! [X0,X1,X2] :
( '>='(X0,X1)
=> '>='('==>'(X1,X2),'==>'(X0,X2)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_10) ).
fof(f11,axiom,
! [X0,X1,X2] :
( '>='(X0,X1)
=> '>='('==>'(X2,X0),'==>'(X2,X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_11) ).
fof(f12,axiom,
! [X0] : '+'(X0,'1') = '1',
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_12) ).
fof(f13,axiom,
! [X0,X1] : '==>'('==>'(X0,X1),X1) = '==>'('==>'(X1,X0),X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_13) ).
fof(f14,conjecture,
! [X0,X1] : '+'(X0,'==>'(X0,X1)) = '+'(X1,'==>'(X1,X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goals_14) ).
fof(f15,negated_conjecture,
~ ! [X0,X1] : '+'(X0,'==>'(X0,X1)) = '+'(X1,'==>'(X1,X0)),
inference(negated_conjecture,[status(cth)],[f14]) ).
fof(f16,plain,
! [X0,X1,X2] :
( '>='(X0,X2)
| ~ '>='(X0,X1)
| ~ '>='(X1,X2) ),
inference(ennf_transformation,[],[f5]) ).
fof(f17,plain,
! [X0,X1,X2] :
( '>='(X0,X2)
| ~ '>='(X0,X1)
| ~ '>='(X1,X2) ),
inference(flattening,[],[f16]) ).
fof(f18,plain,
! [X0,X1] :
( X0 = X1
| ~ '>='(X0,X1)
| ~ '>='(X1,X0) ),
inference(ennf_transformation,[],[f6]) ).
fof(f19,plain,
! [X0,X1] :
( X0 = X1
| ~ '>='(X0,X1)
| ~ '>='(X1,X0) ),
inference(flattening,[],[f18]) ).
fof(f20,plain,
! [X0,X1,X2] :
( '>='('+'(X0,X2),'+'(X1,X2))
| ~ '>='(X0,X1) ),
inference(ennf_transformation,[],[f9]) ).
fof(f21,plain,
! [X0,X1,X2] :
( '>='('==>'(X1,X2),'==>'(X0,X2))
| ~ '>='(X0,X1) ),
inference(ennf_transformation,[],[f10]) ).
fof(f22,plain,
! [X0,X1,X2] :
( '>='('==>'(X2,X0),'==>'(X2,X1))
| ~ '>='(X0,X1) ),
inference(ennf_transformation,[],[f11]) ).
fof(f23,plain,
? [X0,X1] : '+'(X0,'==>'(X0,X1)) != '+'(X1,'==>'(X1,X0)),
inference(ennf_transformation,[],[f15]) ).
fof(f24,plain,
! [X0,X1,X2] :
( ( '>='('+'(X0,X1),X2)
| ~ '>='(X1,'==>'(X0,X2)) )
& ( '>='(X1,'==>'(X0,X2))
| ~ '>='('+'(X0,X1),X2) ) ),
inference(nnf_transformation,[],[f7]) ).
fof(f25,plain,
'+'(sK0,'==>'(sK0,sK1)) != '+'(sK1,'==>'(sK1,sK0)),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1]),skolemize(X0,sK0),skolemize(X1,sK1)],[f23]) ).
fof(f26,plain,
! [X2,X0,X1] : '+'('+'(X0,X1),X2) = '+'(X0,'+'(X1,X2)),
inference(cnf_transformation,[],[f1]) ).
fof(f27,plain,
! [X0,X1] : '+'(X0,X1) = '+'(X1,X0),
inference(cnf_transformation,[],[f2]) ).
fof(f28,plain,
! [X0] : '+'(X0,'0') = X0,
inference(cnf_transformation,[],[f3]) ).
fof(f29,plain,
! [X0] : '>='(X0,X0),
inference(cnf_transformation,[],[f4]) ).
fof(f30,plain,
! [X2,X0,X1] :
( ~ '>='(X1,X2)
| ~ '>='(X0,X1)
| '>='(X0,X2) ),
inference(cnf_transformation,[],[f17]) ).
fof(f31,plain,
! [X0,X1] :
( ~ '>='(X1,X0)
| ~ '>='(X0,X1)
| X0 = X1 ),
inference(cnf_transformation,[],[f19]) ).
fof(f32,plain,
! [X2,X0,X1] :
( ~ '>='('+'(X0,X1),X2)
| '>='(X1,'==>'(X0,X2)) ),
inference(cnf_transformation,[],[f24]) ).
fof(f33,plain,
! [X2,X0,X1] :
( ~ '>='(X1,'==>'(X0,X2))
| '>='('+'(X0,X1),X2) ),
inference(cnf_transformation,[],[f24]) ).
fof(f34,plain,
! [X0] : '>='(X0,'0'),
inference(cnf_transformation,[],[f8]) ).
fof(f35,plain,
! [X2,X0,X1] :
( ~ '>='(X0,X1)
| '>='('+'(X0,X2),'+'(X1,X2)) ),
inference(cnf_transformation,[],[f20]) ).
fof(f36,plain,
! [X2,X0,X1] :
( ~ '>='(X0,X1)
| '>='('==>'(X1,X2),'==>'(X0,X2)) ),
inference(cnf_transformation,[],[f21]) ).
fof(f37,plain,
! [X2,X0,X1] :
( ~ '>='(X0,X1)
| '>='('==>'(X2,X0),'==>'(X2,X1)) ),
inference(cnf_transformation,[],[f22]) ).
fof(f38,plain,
! [X0] : '1' = '+'(X0,'1'),
inference(cnf_transformation,[],[f12]) ).
fof(f39,plain,
! [X0,X1] : '==>'('==>'(X0,X1),X1) = '==>'('==>'(X1,X0),X0),
inference(cnf_transformation,[],[f13]) ).
fof(f40,plain,
'+'(sK0,'==>'(sK0,sK1)) != '+'(sK1,'==>'(sK1,sK0)),
inference(cnf_transformation,[],[f25]) ).
fof(f41,plain,
! [X0] : '+'('0',X0) = X0,
inference(superposition,[],[f27,f28]) ).
fof(f60,plain,
! [X0] :
( ~ '>='('0',X0)
| '0' = X0 ),
inference(resolution,[],[f31,f34]) ).
fof(f63,plain,
! [X0,X1] : '>='(X0,'==>'(X1,'+'(X1,X0))),
inference(resolution,[],[f32,f29]) ).
fof(f65,plain,
! [X0,X1] :
( ~ '>='(X0,X1)
| '>='('0','==>'(X0,X1)) ),
inference(superposition,[],[f32,f28]) ).
fof(f67,plain,
! [X2,X0,X1] :
( ~ '>='('+'(X0,X1),X2)
| '>='(X0,'==>'(X1,X2)) ),
inference(superposition,[],[f32,f27]) ).
fof(f71,plain,
! [X0,X1] : '>='('+'(X0,'==>'(X0,X1)),X1),
inference(resolution,[],[f33,f29]) ).
fof(f80,plain,
! [X0,X1] :
( ~ '>='('==>'(X0,'+'(X0,X1)),X1)
| '==>'(X0,'+'(X0,X1)) = X1 ),
inference(resolution,[],[f63,f31]) ).
fof(f82,plain,
! [X0] : '0' = '==>'(X0,'+'(X0,'0')),
inference(resolution,[],[f63,f60]) ).
fof(f86,plain,
! [X0,X1] : '>='(X0,'==>'(X1,'+'(X0,X1))),
inference(superposition,[],[f63,f27]) ).
fof(f90,plain,
! [X0] : '0' = '==>'(X0,X0),
inference(forward_demodulation,[],[f82,f28]) ).
fof(f117,plain,
! [X0,X1] :
( ~ '>='(X0,'0')
| '>='('+'(X1,X0),X1) ),
inference(superposition,[],[f33,f90]) ).
fof(f122,plain,
! [X0,X1] : '>='('+'(X1,X0),X1),
inference(forward_subsumption_resolution,[],[f117,f34]) ).
fof(f127,plain,
! [X2,X0,X1] : '>='('+'(X0,'+'('==>'(X0,X1),X2)),X1),
inference(resolution,[],[f122,f33]) ).
fof(f129,plain,
! [X0] : '>='('1',X0),
inference(superposition,[],[f122,f38]) ).
fof(f130,plain,
! [X0,X1] : '>='('+'(X0,X1),X1),
inference(superposition,[],[f122,f27]) ).
fof(f135,plain,
! [X0] :
( ~ '>='(X0,'1')
| '1' = X0 ),
inference(resolution,[],[f129,f31]) ).
fof(f136,plain,
! [X0,X1] :
( ~ '>='(X0,'1')
| '>='(X0,X1) ),
inference(resolution,[],[f129,f30]) ).
fof(f139,plain,
! [X0,X1] : '>='(X0,'==>'(X1,X0)),
inference(resolution,[],[f130,f32]) ).
fof(f188,plain,
! [X0,X1] :
( ~ '>='(X0,'+'(X1,'==>'(X1,X0)))
| '+'(X1,'==>'(X1,X0)) = X0 ),
inference(resolution,[],[f71,f31]) ).
fof(f190,plain,
! [X2,X0,X1] : '>='('+'(X0,'+'(X1,'==>'(X1,'==>'(X0,X2)))),X2),
inference(resolution,[],[f71,f33]) ).
fof(f191,plain,
! [X0,X1] : '>='('+'(X0,'==>'(X0,'1')),X1),
inference(resolution,[],[f71,f136]) ).
fof(f195,plain,
! [X0] : '>='('==>'('0',X0),X0),
inference(superposition,[],[f71,f41]) ).
fof(f198,plain,
! [X0] :
( ~ '>='(X0,'==>'('0',X0))
| '==>'('0',X0) = X0 ),
inference(resolution,[],[f195,f31]) ).
fof(f205,plain,
! [X0] : '==>'('0',X0) = X0,
inference(forward_subsumption_resolution,[],[f198,f139]) ).
fof(f219,plain,
! [X0,X1] : '>='('+'(X0,X1),'+'(X1,X0)),
inference(resolution,[],[f86,f33]) ).
fof(f220,plain,
! [X2,X0,X1] : '>='('+'(X0,X1),'+'('==>'(X2,'+'(X0,X2)),X1)),
inference(resolution,[],[f86,f35]) ).
fof(f253,plain,
! [X0,X1] : '>='('==>'(X0,'1'),'==>'(X0,X1)),
inference(resolution,[],[f191,f32]) ).
fof(f286,plain,
! [X0] : '>='('0','==>'('1',X0)),
inference(superposition,[],[f253,f90]) ).
fof(f297,plain,
! [X2,X0,X1] : '>='('==>'('==>'(X0,X1),X2),'==>'(X1,X2)),
inference(resolution,[],[f36,f139]) ).
fof(f320,plain,
! [X0] : '0' = '==>'('1',X0),
inference(resolution,[],[f286,f60]) ).
fof(f378,plain,
! [X0,X1] : '>='('0','==>'('+'(X0,X1),X0)),
inference(resolution,[],[f65,f122]) ).
fof(f396,plain,
! [X0,X1] : '0' = '==>'('+'(X0,X1),X0),
inference(resolution,[],[f378,f60]) ).
fof(f475,plain,
! [X2,X0,X1] : '>='('==>'(X0,'+'(X1,X2)),'==>'(X0,'+'(X2,X1))),
inference(resolution,[],[f37,f219]) ).
fof(f476,plain,
! [X2,X0,X1] : '>='('==>'(X0,'+'(X1,'==>'(X1,X2))),'==>'(X0,X2)),
inference(resolution,[],[f37,f71]) ).
fof(f631,plain,
! [X2,X0,X1] : '+'(X0,'+'(X1,X2)) = '+'(X1,'+'(X2,X0)),
inference(superposition,[],[f26,f27]) ).
fof(f640,plain,
! [X2,X3,X0,X1] :
( ~ '>='('+'(X0,'+'(X1,X2)),X3)
| '>='(X2,'==>'('+'(X0,X1),X3)) ),
inference(superposition,[],[f32,f26]) ).
fof(f654,plain,
! [X2,X0,X1] : '>='('+'(X0,'+'(X1,'==>'('+'(X0,X1),X2))),X2),
inference(superposition,[],[f71,f26]) ).
fof(f810,plain,
! [X0] : '==>'('0',X0) = '==>'('==>'(X0,'1'),'1'),
inference(superposition,[],[f39,f320]) ).
fof(f814,plain,
! [X0,X1] : '>='('+'('==>'(X1,X0),'==>'('==>'(X0,X1),X1)),X0),
inference(superposition,[],[f71,f39]) ).
fof(f861,plain,
! [X0] : '==>'('==>'(X0,'1'),'1') = X0,
inference(forward_demodulation,[],[f810,f205]) ).
fof(f1338,plain,
! [X0,X1] : '1' = '+'(X0,'+'('==>'(X0,'1'),X1)),
inference(resolution,[],[f127,f135]) ).
fof(f2395,plain,
! [X2,X3,X0,X1] :
( ~ '>='('+'(X0,'+'(X1,X2)),X3)
| '>='('+'(X2,X0),'==>'(X1,X3)) ),
inference(superposition,[],[f32,f631]) ).
fof(f6462,plain,
! [X2,X0,X1] : '>='('==>'(X0,'==>'(X1,X2)),'==>'('+'(X1,X0),X2)),
inference(resolution,[],[f190,f640]) ).
fof(f8851,plain,
! [X2,X0,X1] : '>='('+'(X0,'==>'('+'(X1,X0),X2)),'==>'(X1,X2)),
inference(resolution,[],[f654,f32]) ).
fof(f9147,plain,
! [X0,X1] : '>='('==>'(X0,X1),'==>'('==>'('==>'(X1,X0),X0),X1)),
inference(resolution,[],[f814,f67]) ).
fof(f13432,plain,
! [X2,X0,X1] : '>='('+'(X2,X0),'+'(X0,'==>'(X1,'+'(X2,X1)))),
inference(superposition,[],[f220,f27]) ).
fof(f13637,plain,
! [X0,X1] : '==>'(X0,X1) = '==>'(X0,'+'(X0,'==>'(X0,X1))),
inference(resolution,[],[f80,f476]) ).
fof(f16091,plain,
! [X2,X0,X1] : '>='('==>'('+'(X0,X1),X2),'==>'(X1,'==>'(X0,X2))),
inference(resolution,[],[f8851,f32]) ).
fof(f16201,plain,
! [X0,X1] :
( ~ '>='('==>'('==>'('==>'(X0,X1),X1),X0),'==>'(X1,X0))
| '==>'(X1,X0) = '==>'('==>'('==>'(X0,X1),X1),X0) ),
inference(resolution,[],[f9147,f31]) ).
fof(f16294,plain,
! [X0,X1] : '==>'(X1,X0) = '==>'('==>'('==>'(X0,X1),X1),X0),
inference(forward_subsumption_resolution,[],[f16201,f297]) ).
fof(f18505,plain,
! [X2,X0,X1] : '>='('+'('==>'(X0,'==>'(X1,X2)),X1),'==>'(X0,X2)),
inference(resolution,[],[f2395,f190]) ).
fof(f18692,plain,
! [X2,X0,X1] : '>='('+'(X1,'==>'(X0,'==>'(X1,X2))),'==>'(X0,X2)),
inference(forward_demodulation,[],[f18505,f27]) ).
fof(f20968,plain,
! [X0,X1] : '==>'('==>'('+'(X0,'==>'(X0,X1)),X0),X0) = '==>'('==>'(X0,X1),'+'(X0,'==>'(X0,X1))),
inference(superposition,[],[f39,f13637]) ).
fof(f21144,plain,
! [X0,X1] : '==>'('0',X0) = '==>'('==>'(X0,X1),'+'(X0,'==>'(X0,X1))),
inference(forward_demodulation,[],[f20968,f396]) ).
fof(f21178,plain,
! [X0,X1] : '==>'('==>'(X0,X1),'+'(X0,'==>'(X0,X1))) = X0,
inference(forward_demodulation,[],[f21144,f205]) ).
fof(f21983,plain,
! [X2,X0,X1] : '>='('==>'(X0,'==>'(X1,X2)),'==>'(X1,'==>'(X0,X2))),
inference(resolution,[],[f18692,f32]) ).
fof(f22478,plain,
! [X2,X0,X1] :
( ~ '>='('==>'(X0,'+'(X1,X2)),'==>'(X0,'+'(X2,X1)))
| '==>'(X0,'+'(X1,X2)) = '==>'(X0,'+'(X2,X1)) ),
inference(resolution,[],[f475,f31]) ).
fof(f22585,plain,
! [X2,X0,X1] : '==>'(X0,'+'(X1,X2)) = '==>'(X0,'+'(X2,X1)),
inference(forward_subsumption_resolution,[],[f22478,f475]) ).
fof(f23381,plain,
! [X0,X1] : '+'(X1,X0) = '+'(X0,'==>'(X0,'+'(X1,X0))),
inference(resolution,[],[f13432,f188]) ).
fof(f28542,plain,
! [X2,X0,X1] :
( ~ '>='('==>'(X0,'==>'(X1,X2)),'==>'('+'(X1,X0),X2))
| '==>'('+'(X1,X0),X2) = '==>'(X0,'==>'(X1,X2)) ),
inference(resolution,[],[f16091,f31]) ).
fof(f28650,plain,
! [X2,X0,X1] : '==>'('+'(X1,X0),X2) = '==>'(X0,'==>'(X1,X2)),
inference(forward_subsumption_resolution,[],[f28542,f6462]) ).
fof(f45851,plain,
! [X2,X0,X1] :
( ~ '>='('==>'(X0,'==>'(X1,X2)),'==>'(X1,'==>'(X0,X2)))
| '==>'(X1,'==>'(X0,X2)) = '==>'(X0,'==>'(X1,X2)) ),
inference(resolution,[],[f21983,f31]) ).
fof(f45988,plain,
! [X2,X0,X1] : '==>'(X1,'==>'(X0,X2)) = '==>'(X0,'==>'(X1,X2)),
inference(forward_subsumption_resolution,[],[f45851,f21983]) ).
fof(f54591,plain,
! [X0,X1] : '+'(X1,X0) = '+'(X0,'==>'(X0,'+'(X0,X1))),
inference(superposition,[],[f23381,f22585]) ).
fof(f69538,plain,
! [X0,X1] : '==>'(X1,X0) = '==>'('==>'(X0,'1'),'==>'(X1,'1')),
inference(superposition,[],[f45988,f861]) ).
fof(f97762,plain,
! [X0,X1] : '==>'('==>'(X1,'+'(X1,X0)),'+'(X0,X1)) = X1,
inference(superposition,[],[f21178,f54591]) ).
fof(f149929,plain,
! [X0,X1] : '+'('==>'(X0,'1'),X1) = '==>'('==>'('+'('==>'(X0,'1'),X1),'+'('+'('==>'(X0,'1'),X1),X0)),'1'),
inference(superposition,[],[f97762,f1338]) ).
fof(f150702,plain,
! [X0,X1] : '+'('==>'(X0,'1'),X1) = '==>'('==>'('+'('==>'(X0,'1'),X1),'+'(X0,'+'('==>'(X0,'1'),X1))),'1'),
inference(forward_demodulation,[],[f149929,f22585]) ).
fof(f150904,plain,
! [X0,X1] : '+'('==>'(X0,'1'),X1) = '==>'('==>'(X1,'==>'('==>'(X0,'1'),'+'(X0,'+'('==>'(X0,'1'),X1)))),'1'),
inference(forward_demodulation,[],[f150702,f28650]) ).
fof(f151012,plain,
! [X0,X1] : '+'('==>'(X0,'1'),X1) = '==>'('==>'(X1,'==>'('==>'(X0,'1'),'1')),'1'),
inference(forward_demodulation,[],[f150904,f1338]) ).
fof(f151058,plain,
! [X0,X1] : '+'('==>'(X0,'1'),X1) = '==>'('==>'(X1,X0),'1'),
inference(forward_demodulation,[],[f151012,f861]) ).
fof(f249544,plain,
! [X0,X1] : '==>'('==>'(X0,'1'),'==>'(X1,'1')) = '==>'('==>'('==>'(X0,X1),'==>'(X0,'1')),'==>'(X1,'1')),
inference(superposition,[],[f16294,f69538]) ).
fof(f249948,plain,
! [X0,X1] : '==>'('==>'(X0,'1'),'==>'(X1,'1')) = '==>'(X1,'==>'('==>'('==>'(X0,X1),'==>'(X0,'1')),'1')),
inference(forward_demodulation,[],[f249544,f45988]) ).
fof(f250229,plain,
! [X0,X1] : '==>'('==>'(X0,'1'),'==>'(X1,'1')) = '==>'(X1,'+'('==>'('==>'(X0,'1'),'1'),'==>'(X0,X1))),
inference(forward_demodulation,[],[f249948,f151058]) ).
fof(f250374,plain,
! [X0,X1] : '==>'('==>'(X0,'1'),'==>'(X1,'1')) = '==>'(X1,'+'('+'('==>'('1','1'),X0),'==>'(X0,X1))),
inference(forward_demodulation,[],[f250229,f151058]) ).
fof(f250462,plain,
! [X0,X1] : '==>'('==>'(X0,'1'),'==>'(X1,'1')) = '==>'(X1,'+'('==>'('1','1'),'+'(X0,'==>'(X0,X1)))),
inference(forward_demodulation,[],[f250374,f26]) ).
fof(f250511,plain,
! [X0,X1] : '==>'('==>'(X0,'1'),'==>'(X1,'1')) = '==>'(X1,'+'('0','+'(X0,'==>'(X0,X1)))),
inference(forward_demodulation,[],[f250462,f90]) ).
fof(f250547,plain,
! [X0,X1] : '==>'(X1,'+'(X0,'==>'(X0,X1))) = '==>'('==>'(X0,'1'),'==>'(X1,'1')),
inference(forward_demodulation,[],[f250511,f41]) ).
fof(f250573,plain,
! [X0,X1] : '==>'(X1,X0) = '==>'(X1,'+'(X0,'==>'(X0,X1))),
inference(forward_demodulation,[],[f250547,f69538]) ).
fof(f259134,plain,
! [X0,X1] : '>='('+'(X0,'==>'(X0,X1)),'+'(X1,'==>'(X1,X0))),
inference(superposition,[],[f71,f250573]) ).
fof(f260582,plain,
! [X0,X1] :
( ~ '>='('+'(X0,'==>'(X0,X1)),'+'(X1,'==>'(X1,X0)))
| '+'(X0,'==>'(X0,X1)) = '+'(X1,'==>'(X1,X0)) ),
inference(resolution,[],[f259134,f31]) ).
fof(f260879,plain,
! [X0,X1] : '+'(X0,'==>'(X0,X1)) = '+'(X1,'==>'(X1,X0)),
inference(forward_subsumption_resolution,[],[f260582,f259134]) ).
fof(f265999,plain,
'+'(sK0,'==>'(sK0,sK1)) != '+'(sK0,'==>'(sK0,sK1)),
inference(superposition,[],[f40,f260879]) ).
fof(f266000,plain,
$false,
inference(trivial_inequality_removal,[],[f265999]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : LCL900+1 : TPTP v9.3.1. Released v5.5.0.
% 0.00/0.02 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.03/0.31 % Computer : n012.cluster.edu
% 0.03/0.31 % Model : x86_64 x86_64
% 0.03/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.03/0.31 % Memory : 8046.5625MB
% 0.03/0.31 % OS : Linux 6.8.0-71-generic
% 0.03/0.31 % CPULimit : 300
% 0.03/0.31 % WCLimit : 300
% 0.03/0.31 % DateTime : Sun Sep 27 17:05:20 UTC 2026
% 0.03/0.32 % CPUTime :
% 0.03/0.32 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.07/0.33 Running first-order model finding
% 0.07/0.33 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 7.81/1.64 % (2594264)Will run a generic schedule for satisfiability detection.
% 7.81/1.64 % (2594270)% WARNING: option uhcvi not known.
% 7.81/1.64 % (2594271)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=951108587:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 7.81/1.64 % (2594274)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3562998332:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 7.81/1.64 % (2594269)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=97654552_2999 on theBenchmark for (2999ds/0Mi)
% 7.81/1.64 % (2594270)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=240392392:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 7.81/1.64 % (2594272)dis+10_1_sil=32000:sp=arity:random_seed=2990044216:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 7.81/1.64 % (2594273)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=64864:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 7.81/1.64 % (2594275)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=4086423931:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 7.81/1.64 % TRYING [1]
% 7.81/1.64 % TRYING [2]
% 7.81/1.64 % TRYING [3]
% 7.81/1.64 % TRYING [4]
% 7.81/1.64 % TRYING [5]
% 7.81/1.64 % TRYING [6]
% 7.81/1.64 % (2594272)Instruction limit reached!
% 7.81/1.64 % (2594272)------------------------------
% 7.81/1.64 % (2594272)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.81/1.64 % (2594272)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.81/1.64 % (2594272)CaDiCaL version: 2.1.3
% 7.81/1.64 % (2594272)Termination reason: Instruction limit
% 7.81/1.64 % (2594272)Termination phase: Saturation
% 7.81/1.64 % (2594272)Time elapsed: 0.034 s
% 7.81/1.64 % (2594272)Peak memory usage: 12 MB
% 7.81/1.64 % (2594272)Instructions burned: 104 (million)
% 7.81/1.64 % (2594273)Instruction limit reached!
% 7.81/1.64 % (2594273)------------------------------
% 7.81/1.64 % (2594273)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.81/1.64 % (2594273)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.81/1.64 % (2594273)CaDiCaL version: 2.1.3
% 7.81/1.64 % (2594273)Termination reason: Instruction limit
% 7.81/1.64 % (2594273)Termination phase: Saturation
% 7.81/1.64 % (2594273)Time elapsed: 0.036 s
% 7.81/1.64 % (2594273)Peak memory usage: 12 MB
% 7.81/1.64 % (2594273)Instructions burned: 117 (million)
% 7.81/1.64 % (2594274)Instruction limit reached!
% 7.81/1.64 % (2594274)------------------------------
% 7.81/1.64 % (2594274)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.81/1.64 % (2594274)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.81/1.64 % (2594274)CaDiCaL version: 2.1.3
% 7.81/1.64 % (2594274)Termination reason: Instruction limit
% 7.81/1.64 % (2594274)Termination phase: Saturation
% 7.81/1.64 % (2594274)Time elapsed: 0.043 s
% 7.81/1.64 % (2594274)Peak memory usage: 12 MB
% 7.81/1.64 % (2594274)Instructions burned: 133 (million)
% 7.81/1.64 % (2594283)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3631320271:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 7.81/1.64 % TRYING [1]
% 7.81/1.64 % TRYING [2]
% 7.81/1.64 % (2594284)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1318672102:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 7.81/1.64 % TRYING [3]
% 7.81/1.64 % TRYING [4]
% 7.81/1.64 % (2594285)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=3624222975:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 7.81/1.64 % (2594275)Instruction limit reached!
% 7.81/1.64 % (2594275)------------------------------
% 7.81/1.64 % (2594275)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.81/1.64 % (2594275)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.81/1.64 % (2594275)CaDiCaL version: 2.1.3
% 7.81/1.64 % (2594275)Termination reason: Instruction limit
% 7.81/1.64 % (2594275)Termination phase: Saturation
% 7.81/1.64 % (2594275)Time elapsed: 0.055 s
% 7.81/1.64 % (2594275)Peak memory usage: 12 MB
% 7.81/1.64 % (2594275)Instructions burned: 159 (million)
% 7.81/1.64 % TRYING [5]
% 7.81/1.64 % (2594289)ott-21_1_sil=16000:fs=off:random_seed=4209121887:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi)
% 7.81/1.64 % TRYING [6]
% 7.81/1.64 % TRYING [7]
% 7.81/1.64 % (2594284)Instruction limit reached!
% 7.81/1.64 % (2594284)------------------------------
% 7.81/1.64 % (2594284)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.16/4.00 % (2594284)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.16/4.00 % (2594284)CaDiCaL version: 2.1.3
% 24.16/4.00 % (2594284)Termination reason: Instruction limit
% 24.16/4.00 % (2594284)Termination phase: Saturation
% 24.16/4.00 % (2594284)Time elapsed: 0.046 s
% 24.16/4.00 % (2594284)Peak memory usage: 13 MB
% 24.16/4.00 % (2594284)Instructions burned: 133 (million)
% 24.16/4.00 % (2594291)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2157569772:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 24.16/4.00 % (2594289)Instruction limit reached!
% 24.16/4.00 % (2594289)------------------------------
% 24.16/4.00 % (2594289)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.16/4.00 % (2594289)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.16/4.00 % (2594289)CaDiCaL version: 2.1.3
% 24.16/4.00 % (2594289)Termination reason: Instruction limit
% 24.16/4.00 % (2594289)Termination phase: Saturation
% 24.16/4.00 % (2594289)Time elapsed: 0.039 s
% 24.16/4.00 % (2594289)Peak memory usage: 12 MB
% 24.16/4.00 % (2594289)Instructions burned: 180 (million)
% 24.16/4.00 % (2594293)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1601504648:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 24.16/4.00 % TRYING [1]
% 24.16/4.00 % TRYING [2]
% 24.16/4.00 % TRYING [3]
% 24.16/4.00 % TRYING [4]
% 24.16/4.00 % TRYING [7]
% 24.16/4.00 % TRYING [5]
% 24.16/4.00 % TRYING [6]
% 24.16/4.00 % TRYING [7]
% 24.16/4.00 % (2594283)Instruction limit reached!
% 24.16/4.00 % (2594283)------------------------------
% 24.16/4.00 % (2594283)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.16/4.00 % (2594283)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.16/4.00 % (2594283)CaDiCaL version: 2.1.3
% 24.16/4.00 % (2594283)Termination reason: Instruction limit
% 24.16/4.00 % (2594283)Termination phase: Finite model building SAT solving
% 24.16/4.00 % (2594283)Time elapsed: 0.188 s
% 24.16/4.00 % (2594283)Peak memory usage: 25 MB
% 24.16/4.00 % (2594283)Instructions burned: 716 (million)
% 24.16/4.00 % (2594295)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=490367512:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 24.16/4.00 % (2594285)Instruction limit reached!
% 24.16/4.00 % (2594285)------------------------------
% 24.16/4.00 % (2594285)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.16/4.00 % (2594285)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.16/4.00 % (2594285)CaDiCaL version: 2.1.3
% 24.16/4.00 % (2594285)Termination reason: Instruction limit
% 24.16/4.00 % (2594285)Termination phase: Saturation
% 24.16/4.00 % (2594285)Time elapsed: 0.199 s
% 24.16/4.00 % (2594285)Peak memory usage: 17 MB
% 24.16/4.00 % (2594285)Instructions burned: 685 (million)
% 24.16/4.00 % (2594297)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1232249453:i=889:ins=1_2997 on theBenchmark for (2997ds/889Mi)
% 24.16/4.00 % (2594291)Instruction limit reached!
% 24.16/4.00 % (2594291)------------------------------
% 24.16/4.00 % (2594291)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.16/4.00 % (2594291)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.16/4.00 % (2594291)CaDiCaL version: 2.1.3
% 24.16/4.00 % (2594291)Termination reason: Instruction limit
% 24.16/4.00 % (2594291)Termination phase: Saturation
% 24.16/4.00 % (2594291)Time elapsed: 0.162 s
% 24.16/4.00 % (2594291)Peak memory usage: 13 MB
% 24.16/4.00 % (2594291)Instructions burned: 478 (million)
% 24.16/4.00 % (2594299)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=2004677060:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2997 on theBenchmark for (2997ds/692Mi)
% 24.16/4.00 % TRYING [14]
% 24.16/4.00 % TRYING [8]
% 24.16/4.00 % (2594293)Instruction limit reached!
% 24.16/4.00 % (2594293)------------------------------
% 24.16/4.00 % (2594293)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.16/4.00 % (2594293)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.16/4.00 % (2594293)CaDiCaL version: 2.1.3
% 24.16/4.00 % (2594293)Termination reason: Instruction limit
% 24.16/4.00 % (2594293)Termination phase: Finite model building SAT solving
% 24.16/4.00 % (2594293)Time elapsed: 0.191 s
% 24.16/4.00 % (2594293)Peak memory usage: 21 MB
% 24.16/4.00 % (2594293)Instructions burned: 871 (million)
% 24.16/4.00 % (2594301)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2183465998:i=879:kws=inv_precedence:fsr=off_2996 on theBenchmark for (2996ds/879Mi)
% 56.72/8.45 % (2594297)Instruction limit reached!
% 56.72/8.45 % (2594297)------------------------------
% 56.72/8.45 % (2594297)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 56.72/8.45 % (2594297)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 56.72/8.45 % (2594297)CaDiCaL version: 2.1.3
% 56.72/8.45 % (2594297)Termination reason: Instruction limit
% 56.72/8.45 % (2594297)Termination phase: Finite model building constraint generation
% 56.72/8.45 % (2594297)Time elapsed: 0.183 s
% 56.72/8.45 % (2594297)Peak memory usage: 80 MB
% 56.72/8.45 % (2594297)Instructions burned: 890 (million)
% 56.72/8.45 % (2594303)fmb+10_1_sil=64000:random_seed=3963094336:i=22061:nm=2:gsp=on_2995 on theBenchmark for (2995ds/22061Mi)
% 56.72/8.45 % TRYING [1]
% 56.72/8.45 % TRYING [2]
% 56.72/8.45 % TRYING [3]
% 56.72/8.45 % TRYING [4]
% 56.72/8.45 % (2594299)Instruction limit reached!
% 56.72/8.45 % (2594299)------------------------------
% 56.72/8.45 % (2594299)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 56.72/8.45 % (2594299)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 56.72/8.45 % (2594299)CaDiCaL version: 2.1.3
% 56.72/8.45 % (2594299)Termination reason: Instruction limit
% 56.72/8.45 % (2594299)Termination phase: Saturation
% 56.72/8.45 % (2594299)Time elapsed: 0.197 s
% 56.72/8.45 % (2594299)Peak memory usage: 16 MB
% 56.72/8.45 % (2594299)Instructions burned: 692 (million)
% 56.72/8.45 % TRYING [5]
% 56.72/8.45 % (2594305)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1361843136:i=9515:nm=5_2994 on theBenchmark for (2994ds/9515Mi)
% 56.72/8.45 % TRYING [20]
% 56.72/8.45 % TRYING [6]
% 56.72/8.45 % TRYING [7]
% 56.72/8.45 % (2594301)Instruction limit reached!
% 56.72/8.45 % (2594301)------------------------------
% 56.72/8.45 % (2594301)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 56.72/8.45 % (2594301)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 56.72/8.45 % (2594301)CaDiCaL version: 2.1.3
% 56.72/8.45 % (2594301)Termination reason: Instruction limit
% 56.72/8.45 % (2594301)Termination phase: Saturation
% 56.72/8.45 % (2594301)Time elapsed: 0.271 s
% 56.72/8.45 % (2594301)Peak memory usage: 17 MB
% 56.72/8.45 % (2594301)Instructions burned: 879 (million)
% 56.72/8.45 % (2594307)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2340725490:fmbsr=1.7:i=920_2993 on theBenchmark for (2993ds/920Mi)
% 56.72/8.45 % TRYING [8]
% 56.72/8.45 % (2594295)Instruction limit reached!
% 56.72/8.45 % (2594295)------------------------------
% 56.72/8.45 % (2594295)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 56.72/8.45 % (2594295)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 56.72/8.45 % (2594295)CaDiCaL version: 2.1.3
% 56.72/8.45 % (2594295)Termination reason: Instruction limit
% 56.72/8.45 % (2594295)Termination phase: Saturation
% 56.72/8.45 % (2594295)Time elapsed: 0.385 s
% 56.72/8.45 % (2594295)Peak memory usage: 23 MB
% 56.72/8.45 % (2594295)Instructions burned: 1180 (million)
% 56.72/8.45 % (2594309)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1393378415:i=5131_2993 on theBenchmark for (2993ds/5131Mi)
% 56.72/8.45 % TRYING [8]
% 56.72/8.45 % TRYING [9]
% 56.72/8.45 % (2594307)Instruction limit reached!
% 56.72/8.45 % (2594307)------------------------------
% 56.72/8.45 % (2594307)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 56.72/8.45 % (2594307)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 56.72/8.45 % (2594307)CaDiCaL version: 2.1.3
% 56.72/8.45 % (2594307)Termination reason: Instruction limit
% 56.72/8.45 % (2594307)Termination phase: Finite model building SAT solving
% 56.72/8.45 % (2594307)Time elapsed: 0.267 s
% 56.72/8.45 % (2594307)Peak memory usage: 40 MB
% 56.72/8.45 % (2594307)Instructions burned: 920 (million)
% 56.72/8.45 % (2594311)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2199585619:i=1472:ins=7:fdi=8:gsp=on_2990 on theBenchmark for (2990ds/1472Mi)
% 56.72/8.45 % TRYING [9]
% 56.72/8.45 % (2594311)Instruction limit reached!
% 56.72/8.45 % (2594311)------------------------------
% 56.72/8.45 % (2594311)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 56.72/8.45 % (2594311)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 56.72/8.45 % (2594311)CaDiCaL version: 2.1.3
% 56.72/8.45 % (2594311)Termination reason: Instruction limit
% 56.72/8.45 % (2594311)Termination phase: Saturation
% 56.72/8.45 % (2594311)Time elapsed: 0.379 s
% 56.72/8.45 % (2594311)Peak memory usage: 23 MB
% 56.72/8.45 % (2594311)Instructions burned: 1472 (million)
% 56.72/8.45 % (2594313)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=689993224:i=6324_2987 on theBenchmark for (2987ds/6324Mi)
% 189.34/27.23 % TRYING [77]
% 189.34/27.23 % TRYING [10]
% 189.34/27.23 % (2594309)Instruction limit reached!
% 189.34/27.23 % (2594309)------------------------------
% 189.34/27.23 % (2594309)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 189.34/27.23 % (2594309)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 189.34/27.23 % (2594309)CaDiCaL version: 2.1.3
% 189.34/27.23 % (2594309)Termination reason: Instruction limit
% 189.34/27.23 % (2594309)Termination phase: Saturation
% 189.34/27.23 % (2594309)Time elapsed: 1.343 s
% 189.34/27.23 % (2594309)Peak memory usage: 31 MB
% 189.34/27.23 % (2594309)Instructions burned: 5133 (million)
% 189.34/27.23 % (2594315)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1116628058:fmbsr=2.30978:i=2174_2979 on theBenchmark for (2979ds/2174Mi)
% 189.34/27.23 % TRYING [16]
% 189.34/27.23 % TRYING [10]
% 189.34/27.23 % (2594315)Instruction limit reached!
% 189.34/27.23 % (2594315)------------------------------
% 189.34/27.23 % (2594315)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 189.34/27.23 % (2594315)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 189.34/27.23 % (2594315)CaDiCaL version: 2.1.3
% 189.34/27.23 % (2594315)Termination reason: Instruction limit
% 189.34/27.23 % (2594315)Termination phase: Finite model building constraint generation
% 189.34/27.23 % (2594315)Time elapsed: 0.403 s
% 189.34/27.23 % (2594315)Peak memory usage: 132 MB
% 189.34/27.23 % (2594315)Instructions burned: 2179 (million)
% 189.34/27.23 % (2594317)ott-2_1_sil=16000:newcnf=on:random_seed=881415670:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2975 on theBenchmark for (2975ds/869Mi)
% 189.34/27.23 % (2594313)Instruction limit reached!
% 189.34/27.23 % (2594313)------------------------------
% 189.34/27.23 % (2594313)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 189.34/27.23 % (2594313)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 189.34/27.23 % (2594313)CaDiCaL version: 2.1.3
% 189.34/27.23 % (2594313)Termination reason: Instruction limit
% 189.34/27.23 % (2594313)Termination phase: Finite model building constraint generation
% 189.34/27.23 % (2594313)Time elapsed: 1.281 s
% 189.34/27.23 % (2594313)Peak memory usage: 424 MB
% 189.34/27.23 % (2594313)Instructions burned: 6326 (million)
% 189.34/27.23 % (2594305)Instruction limit reached!
% 189.34/27.23 % (2594305)------------------------------
% 189.34/27.23 % (2594305)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 189.34/27.23 % (2594305)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 189.34/27.23 % (2594305)CaDiCaL version: 2.1.3
% 189.34/27.23 % (2594305)Termination reason: Instruction limit
% 189.34/27.23 % (2594305)Termination phase: Finite model building constraint generation
% 189.34/27.23 % (2594305)Time elapsed: 2.092 s
% 189.34/27.23 % (2594305)Peak memory usage: 662 MB
% 189.34/27.23 % (2594305)Instructions burned: 9516 (million)
% 189.34/27.23 % (2594319)ott+10_1_sil=32000:tgt=ground:random_seed=3069737677:i=5114:av=off_2973 on theBenchmark for (2973ds/5114Mi)
% 189.34/27.23 % (2594321)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=286631372:i=54282_2973 on theBenchmark for (2973ds/54282Mi)
% 189.34/27.23 % TRYING [1]
% 189.34/27.23 % TRYING [2]
% 189.34/27.23 % TRYING [3]
% 189.34/27.23 % TRYING [4]
% 189.34/27.23 % TRYING [5]
% 189.34/27.23 % TRYING [6]
% 189.34/27.23 % (2594317)Instruction limit reached!
% 189.34/27.23 % (2594317)------------------------------
% 189.34/27.23 % (2594317)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 189.34/27.23 % (2594317)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 189.34/27.23 % (2594317)CaDiCaL version: 2.1.3
% 189.34/27.23 % (2594317)Termination reason: Instruction limit
% 189.34/27.23 % (2594317)Termination phase: Saturation
% 189.34/27.23 % (2594317)Time elapsed: 0.280 s
% 189.34/27.23 % (2594317)Peak memory usage: 17 MB
% 189.34/27.23 % (2594317)Instructions burned: 869 (million)
% 189.34/27.23 % (2594323)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=851823387:i=3512:aac=none_2972 on theBenchmark for (2972ds/3512Mi)
% 189.34/27.23 % TRYING [7]
% 189.34/27.23 % TRYING [8]
% 189.34/27.23 % TRYING [9]
% 189.34/27.23 % (2594323)Instruction limit reached!
% 189.34/27.23 % (2594323)------------------------------
% 189.34/27.23 % (2594323)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 189.34/27.23 % (2594323)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 189.34/27.23 % (2594323)CaDiCaL version: 2.1.3
% 189.34/27.23 % (2594323)Termination reason: Instruction limit
% 189.34/27.23 % (2594323)Termination phase: Saturation
% 189.34/27.23 % (2594323)Time elapsed: 0.918 s
% 189.34/27.23 % (2594323)Peak memory usage: 25 MB
% 198.17/33.15 % (2594323)Instructions burned: 3514 (million)
% 198.17/33.15 % (2594325)dis+21_1_sil=32000:sas=cadical:random_seed=404934309:i=3773:amm=off_2963 on theBenchmark for (2963ds/3773Mi)
% 198.17/33.15 % (2594319)Instruction limit reached!
% 198.17/33.15 % (2594319)------------------------------
% 198.17/33.15 % (2594319)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 198.17/33.15 % (2594319)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 198.17/33.15 % (2594319)CaDiCaL version: 2.1.3
% 198.17/33.15 % (2594319)Termination reason: Instruction limit
% 198.17/33.15 % (2594319)Termination phase: Saturation
% 198.17/33.15 % (2594319)Time elapsed: 1.621 s
% 198.17/33.15 % (2594319)Peak memory usage: 42 MB
% 198.17/33.15 % (2594319)Instructions burned: 5116 (million)
% 198.17/33.15 % (2594327)ott+11_1_sil=16000:gs=on:random_seed=3738065529:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2957 on theBenchmark for (2957ds/2251Mi)
% 198.17/33.15 % TRYING [11]
% 198.17/33.15 % (2594325)Instruction limit reached!
% 198.17/33.15 % (2594325)------------------------------
% 198.17/33.15 % (2594325)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 198.17/33.15 % (2594325)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 198.17/33.15 % (2594325)CaDiCaL version: 2.1.3
% 198.17/33.15 % (2594325)Termination reason: Instruction limit
% 198.17/33.15 % (2594325)Termination phase: Saturation
% 198.17/33.15 % (2594325)Time elapsed: 1.053 s
% 198.17/33.15 % (2594325)Peak memory usage: 31 MB
% 198.17/33.15 % (2594325)Instructions burned: 3776 (million)
% 198.17/33.15 % (2594330)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2849393125:fmbsr=1.6:i=67534_2952 on theBenchmark for (2952ds/67534Mi)
% 198.17/33.15 % TRYING [7]
% 198.17/33.15 % TRYING [10]
% 198.17/33.15 % TRYING [8]
% 198.17/33.15 % (2594327)Instruction limit reached!
% 198.17/33.15 % (2594327)------------------------------
% 198.17/33.15 % (2594327)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 198.17/33.15 % (2594327)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 198.17/33.15 % (2594327)CaDiCaL version: 2.1.3
% 198.17/33.15 % (2594327)Termination reason: Instruction limit
% 198.17/33.15 % (2594327)Termination phase: Saturation
% 198.17/33.15 % (2594327)Time elapsed: 0.698 s
% 198.17/33.15 % (2594327)Peak memory usage: 28 MB
% 198.17/33.15 % (2594327)Instructions burned: 2255 (million)
% 198.17/33.15 % (2594332)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3130028272:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2950 on theBenchmark for (2950ds/4591Mi)
% 198.17/33.15 % TRYING [9]
% 198.17/33.15 % (2594303)Instruction limit reached!
% 198.17/33.15 % (2594303)------------------------------
% 198.17/33.15 % (2594303)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 198.17/33.15 % (2594303)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 198.17/33.15 % (2594303)CaDiCaL version: 2.1.3
% 198.17/33.15 % (2594303)Termination reason: Instruction limit
% 198.17/33.15 % (2594303)Termination phase: Finite model building SAT solving
% 198.17/33.15 % (2594303)Time elapsed: 6.099 s
% 198.17/33.15 % (2594303)Peak memory usage: 99 MB
% 198.17/33.15 % (2594303)Instructions burned: 22062 (million)
% 198.17/33.15 % (2594334)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=453410527:i=29340_2934 on theBenchmark for (2934ds/29340Mi)
% 198.17/33.15 % (2594332)Instruction limit reached!
% 198.17/33.15 % (2594332)------------------------------
% 198.17/33.15 % (2594332)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 198.17/33.15 % (2594332)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 198.17/33.15 % (2594332)CaDiCaL version: 2.1.3
% 198.17/33.15 % (2594332)Termination reason: Instruction limit
% 198.17/33.15 % (2594332)Termination phase: Saturation
% 198.17/33.15 % (2594332)Time elapsed: 1.668 s
% 198.17/33.15 % (2594332)Peak memory usage: 48 MB
% 198.17/33.15 % (2594332)Instructions burned: 4592 (million)
% 198.17/33.15 % (2594336)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=579316583:i=5211_2933 on theBenchmark for (2933ds/5211Mi)
% 198.17/33.15 % TRYING [10]
% 198.17/33.15 % (2594336)Instruction limit reached!
% 198.17/33.15 % (2594336)------------------------------
% 198.17/33.15 % (2594336)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 198.17/33.15 % (2594336)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 198.17/33.15 % (2594336)CaDiCaL version: 2.1.3
% 198.17/33.15 % (2594336)Termination reason: Instruction limit
% 198.17/33.15 % (2594336)Termination phase: Saturation
% 198.17/33.15 % (2594336)Time elapsed: 1.456 s
% 198.17/33.15 % (2594336)Peak memory usage: 40 MB
% 198.17/33.15 % (2594336)Instructions burned: 5212 (million)
% 198.17/33.15 % (2594338)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=4150293154:i=5497:nm=2_2918 on theBenchmark for (2918ds/5497Mi)
% 198.17/33.15 % TRYING [17]
% 198.17/33.15 % TRYING [11]
% 198.17/33.15 % (2594338)Instruction limit reached!
% 198.17/33.15 % (2594338)------------------------------
% 198.17/33.15 % (2594338)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 198.17/33.15 % (2594338)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 198.17/33.15 % (2594338)CaDiCaL version: 2.1.3
% 198.17/33.15 % (2594338)Termination reason: Instruction limit
% 198.17/33.15 % (2594338)Termination phase: Finite model building constraint generation
% 198.17/33.15 % (2594338)Time elapsed: 1.196 s
% 198.17/33.15 % (2594338)Peak memory usage: 383 MB
% 198.17/33.15 % (2594338)Instructions burned: 5497 (million)
% 198.17/33.15 % (2594340)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=2857955839:fmbsr=2:i=46332_2906 on theBenchmark for (2906ds/46332Mi)
% 198.17/33.15 % TRYING [15]
% 198.17/33.15 % TRYING [11]
% 198.17/33.15 % TRYING [11]
% 198.17/33.15 % (2594334)Instruction limit reached!
% 198.17/33.15 % (2594334)------------------------------
% 198.17/33.15 % (2594334)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 198.17/33.15 % (2594334)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 198.17/33.15 % (2594334)CaDiCaL version: 2.1.3
% 198.17/33.15 % (2594334)Termination reason: Instruction limit
% 198.17/33.15 % (2594334)Termination phase: Saturation
% 198.17/33.15 % (2594334)Time elapsed: 8.450 s
% 198.17/33.15 % (2594334)Peak memory usage: 217 MB
% 198.17/33.15 % (2594334)Instructions burned: 29345 (million)
% 198.17/33.15 % (2594342)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=3847821496:i=14071_2849 on theBenchmark for (2849ds/14071Mi)
% 198.17/33.15 % TRYING [12]
% 198.17/33.15 % (2594342)Instruction limit reached!
% 198.17/33.15 % (2594342)------------------------------
% 198.17/33.15 % (2594342)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 198.17/33.15 % (2594342)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 198.17/33.15 % (2594342)CaDiCaL version: 2.1.3
% 198.17/33.15 % (2594342)Termination reason: Instruction limit
% 198.17/33.15 % (2594342)Termination phase: Finite model building SAT solving
% 198.17/33.15 % (2594342)Time elapsed: 6.184 s
% 198.17/33.15 % (2594342)Peak memory usage: 228 MB
% 198.17/33.15 % (2594342)Instructions burned: 14073 (million)
% 198.17/33.15 % (2594464)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=658664029:i=22565:add=on:rawr=on_2787 on theBenchmark for (2787ds/22565Mi)
% 198.17/33.15 % (2594321)Instruction limit reached!
% 198.17/33.15 % (2594321)------------------------------
% 198.17/33.15 % (2594321)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 198.17/33.15 % (2594321)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 198.17/33.15 % (2594321)CaDiCaL version: 2.1.3
% 198.17/33.15 % (2594321)Termination reason: Instruction limit
% 198.17/33.15 % (2594321)Termination phase: Finite model building SAT solving
% 198.17/33.15 % (2594321)Time elapsed: 20.721 s
% 198.17/33.15 % (2594321)Peak memory usage: 174 MB
% 198.17/33.15 % (2594321)Instructions burned: 54283 (million)
% 198.17/33.15 % (2594467)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=470008696:i=8173:av=off_2765 on theBenchmark for (2765ds/8173Mi)
% 198.17/33.15 % (2594467)Instruction limit reached!
% 198.17/33.15 % (2594467)------------------------------
% 198.17/33.15 % (2594467)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 198.17/33.15 % (2594467)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 198.17/33.15 % (2594467)CaDiCaL version: 2.1.3
% 198.17/33.15 % (2594467)Termination reason: Instruction limit
% 198.17/33.15 % (2594467)Termination phase: Saturation
% 198.17/33.15 % (2594467)Time elapsed: 2.543 s
% 198.17/33.15 % (2594467)Peak memory usage: 44 MB
% 198.17/33.15 % (2594467)Instructions burned: 8174 (million)
% 198.17/33.15 % (2594469)dis+10_16:1_sil=16000:random_seed=4178843694:i=9155:fsr=off_2740 on theBenchmark for (2740ds/9155Mi)
% 198.17/33.15 % (2594271)Instruction limit reached!
% 198.17/33.15 % (2594271)------------------------------
% 198.17/33.15 % (2594271)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 198.17/33.15 % (2594271)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 198.17/33.15 % (2594271)CaDiCaL version: 2.1.3
% 198.17/33.15 % (2594271)Termination reason: Instruction limit
% 198.17/33.15 % (2594271)Termination phase: Saturation
% 198.17/33.15 % (2594271)Time elapsed: 26.861 s
% 198.17/33.15 % (2594271)Peak memory usage: 941 MB
% 198.17/33.15 % (2594271)Instructions burned: 88024 (million)
% 198.17/33.15 % (2594471)ott-3_8_sil=64000:random_seed=238941846:i=20139:bs=on_2730 on theBenchmark for (2730ds/20139Mi)
% 198.17/33.15 % (2594464)Instruction limit reached!
% 198.17/33.15 % (2594464)------------------------------
% 198.17/33.15 % (2594464)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 198.17/33.15 % (2594464)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 198.17/33.15 % (2594464)CaDiCaL version: 2.1.3
% 198.17/33.15 % (2594464)Termination reason: Instruction limit
% 198.17/33.15 % (2594464)Termination phase: Saturation
% 198.17/33.15 % (2594464)Time elapsed: 6.957 s
% 198.17/33.15 % (2594464)Peak memory usage: 364 MB
% 198.17/33.15 % (2594464)Instructions burned: 22565 (million)
% 198.17/33.15 % (2594473)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=3427758850:fmbsr=2:i=32576_2717 on theBenchmark for (2717ds/32576Mi)
% 198.17/33.15 % TRYING [9]
% 198.17/33.15 % (2594469)Instruction limit reached!
% 198.17/33.15 % (2594469)------------------------------
% 198.17/33.15 % (2594469)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 198.17/33.15 % (2594469)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 198.17/33.15 % (2594469)CaDiCaL version: 2.1.3
% 198.17/33.15 % (2594469)Termination reason: Instruction limit
% 198.17/33.15 % (2594469)Termination phase: Saturation
% 198.17/33.15 % (2594469)Time elapsed: 2.651 s
% 198.17/33.15 % (2594469)Peak memory usage: 62 MB
% 198.17/33.15 % (2594469)Instructions burned: 9159 (million)
% 198.17/33.15 % (2594476)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=1535609274:i=11404_2713 on theBenchmark for (2713ds/11404Mi)
% 198.17/33.15 % (2594330)Instruction limit reached!
% 198.17/33.15 % (2594330)------------------------------
% 198.17/33.15 % (2594330)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 198.17/33.15 % (2594330)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 198.17/33.15 % (2594330)CaDiCaL version: 2.1.3
% 198.17/33.15 % (2594330)Termination reason: Instruction limit
% 198.17/33.15 % (2594330)Termination phase: Finite model building SAT solving
% 198.17/33.15 % (2594330)Time elapsed: 24.558 s
% 198.17/33.15 % (2594330)Peak memory usage: 119 MB
% 198.17/33.15 % (2594330)Instructions burned: 67534 (million)
% 198.17/33.15 % (2594611)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=571361188:i=14134_2706 on theBenchmark for (2706ds/14134Mi)
% 198.17/33.15 % (2594340)Instruction limit reached!
% 198.17/33.15 % (2594340)------------------------------
% 198.17/33.15 % (2594340)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 198.17/33.15 % (2594340)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 198.17/33.15 % (2594340)CaDiCaL version: 2.1.3
% 198.17/33.15 % (2594340)Termination reason: Instruction limit
% 198.17/33.15 % (2594340)Termination phase: Finite model building SAT solving
% 198.17/33.15 % (2594340)Time elapsed: 20.107 s
% 198.17/33.15 % (2594340)Peak memory usage: 605 MB
% 198.17/33.15 % (2594340)Instructions burned: 46333 (million)
% 198.17/33.15 % (2594620)dis+33_16_sil=32000:sac=on:random_seed=2975509393:i=15851:nm=0_2704 on theBenchmark for (2704ds/15851Mi)
% 198.17/33.15 % TRYING [10]
% 198.17/33.15 % (2594476)Instruction limit reached!
% 198.17/33.15 % (2594476)------------------------------
% 198.17/33.15 % (2594476)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 198.17/33.15 % (2594476)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 198.17/33.15 % (2594476)CaDiCaL version: 2.1.3
% 198.17/33.15 % (2594476)Termination reason: Instruction limit
% 198.17/33.15 % (2594476)Termination phase: Saturation
% 198.17/33.15 % (2594476)Time elapsed: 3.929 s
% 198.17/33.15 % (2594476)Peak memory usage: 58 MB
% 198.17/33.15 % (2594476)Instructions burned: 11407 (million)
% 198.17/33.15 % (2595103)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=3672745561:avsq=on:i=17627:add=on:amm=off_2674 on theBenchmark for (2674ds/17627Mi)
% 198.17/33.15 % (2594620) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2594264-2594620"...
% 198.17/33.15 % (2594620)...printing done.
% 198.17/33.15 % (2594620)Refutation found. Thanks to Tanya!
% 198.17/33.15 % SZS status Theorem for theBenchmark
% 198.17/33.15 % SZS output start Proof for theBenchmark
% See solution above
% 198.17/33.15 % (2594620)------------------------------
% 198.17/33.15 % (2594620)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 198.17/33.15 % (2594620)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 198.17/33.15 % (2594620)CaDiCaL version: 2.1.3
% 198.17/33.15 % (2594620)Termination reason: Refutation
% 198.17/33.15 % (2594620)Time elapsed: 3.218 s
% 198.17/33.15 % (2594620)Peak memory usage: 78 MB
% 198.17/33.15 % (2594620)Instructions burned: 8470 (million)
% 198.17/33.15 % (2594264)Success in time 32.808 s
% 198.17/33.15 % Vampire exiting
%------------------------------------------------------------------------------