%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : BOO020-1 : TPTP v9.3.1. Released v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n009.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 09:36:11 AM UTC 2026
% Result : Unsatisfiable 64.20s 9.39s
% Output : Refutation 64.20s
% Verified :
% SZS Type : Refutation
% Derivation depth : 76
% Number of leaves : 8
% Syntax : Number of formulae : 220 ( 113 unt; 4 def)
% Number of atoms : 342 ( 254 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 241 ( 119 ~; 118 |; 0 &)
% ( 4 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 4 avg)
% Maximal term depth : 9 ( 2 avg)
% Number of predicates : 6 ( 4 usr; 5 prp; 0-2 aty)
% Number of functors : 6 ( 6 usr; 4 con; 0-2 aty)
% Number of variables : 518 ( 0 sgn 518 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0] : add(X0,X0) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',frink1) ).
fof(f2,axiom,
! [X2,X3,X0,X1] :
( add(add(add(X0,X1),X2),X3) != add(add(X1,X2),X0)
| add(add(add(X0,X1),X2),inverse(X3)) = n0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',frink2) ).
fof(f3,axiom,
! [X2,X3,X0,X1] :
( add(add(add(X0,X1),X2),inverse(X3)) != n0
| add(add(add(X0,X1),X2),X3) = add(add(X1,X2),X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',frink3) ).
fof(f4,negated_conjecture,
( add(inverse(add(a,inverse(b))),inverse(add(inverse(a),inverse(b)))) != b
| add(add(a,b),c) != add(a,add(b,c))
| add(b,a) != add(a,b) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_huntington) ).
fof(f5,plain,
( b != add(inverse(add(a,inverse(b))),inverse(add(inverse(a),inverse(b))))
| add(add(a,b),c) != add(a,add(b,c))
| add(a,b) != add(b,a) ),
inference(reorient_equations,[],[f4]) ).
fof(f7,definition,
( spl0_1
<=> add(a,b) = add(b,a) ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f9,plain,
( add(a,b) != add(b,a)
| spl0_1 ),
inference(avatar_component_clause,[],[f7]) ).
fof(f11,definition,
( spl0_2
<=> add(add(a,b),c) = add(a,add(b,c)) ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f13,plain,
( add(add(a,b),c) != add(a,add(b,c))
| spl0_2 ),
inference(avatar_component_clause,[],[f11]) ).
fof(f15,definition,
( spl0_3
<=> b = add(inverse(add(a,inverse(b))),inverse(add(inverse(a),inverse(b)))) ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f17,plain,
( b != add(inverse(add(a,inverse(b))),inverse(add(inverse(a),inverse(b))))
| spl0_3 ),
inference(avatar_component_clause,[],[f15]) ).
fof(f18,plain,
( ~ spl0_1
| ~ spl0_2
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f5,f15,f11,f7]) ).
fof(f25,plain,
! [X2,X0,X1] :
( add(add(X0,X1),X2) != add(add(X0,X1),X0)
| n0 = add(add(X0,X1),inverse(X2)) ),
inference(superposition,[],[f2,f1]) ).
fof(f26,plain,
! [X2,X0,X1] :
( add(add(X0,X1),X2) != add(add(X1,add(X0,X1)),X0)
| n0 = add(add(X0,X1),inverse(X2)) ),
inference(superposition,[],[f2,f1]) ).
fof(f162,plain,
! [X0,X1] : n0 = add(add(X0,X1),inverse(X0)),
inference(equality_resolution,[],[f25]) ).
fof(f269,plain,
! [X0] : n0 = add(X0,inverse(X0)),
inference(superposition,[],[f162,f1]) ).
fof(f276,plain,
! [X0] : n0 = add(n0,inverse(X0)),
inference(superposition,[],[f162,f269]) ).
fof(f431,definition,
( spl0_12
<=> ! [X0] : n0 = add(X0,inverse(inverse(inverse(X0)))) ),
introduced(definition,[new_symbols(definition,[spl0_12])],[avatar_definition]) ).
fof(f432,plain,
( ! [X0] : n0 = add(X0,inverse(inverse(inverse(X0))))
| ~ spl0_12 ),
inference(avatar_component_clause,[],[f431]) ).
fof(f1465,plain,
! [X2,X0,X1] :
( n0 != add(add(X0,X1),inverse(X2))
| add(add(X0,X1),X2) = add(add(X0,X1),X0) ),
inference(superposition,[],[f3,f1]) ).
fof(f1488,plain,
! [X2,X0,X1] :
( n0 != add(n0,inverse(X2))
| add(n0,X2) = add(add(X1,inverse(X0)),X0) ),
inference(superposition,[],[f3,f162]) ).
fof(f1497,plain,
! [X2,X0,X1] :
( n0 != add(add(X0,X1),inverse(X2))
| add(add(X0,X1),X2) = add(add(X1,add(X0,X1)),X0) ),
inference(superposition,[],[f3,f1]) ).
fof(f1518,plain,
! [X2,X0,X1] :
( n0 != n0
| add(add(X1,X2),X0) = add(add(add(X0,X1),X2),add(add(X0,X1),X2)) ),
inference(superposition,[],[f3,f269]) ).
fof(f1541,plain,
! [X2,X0,X1] : add(add(X1,X2),X0) = add(add(add(X0,X1),X2),add(add(X0,X1),X2)),
inference(trivial_inequality_removal,[],[f1518]) ).
fof(f1561,plain,
! [X2,X0,X1] : add(add(X0,X1),X2) = add(add(X1,X2),X0),
inference(forward_demodulation,[],[f1541,f1]) ).
fof(f1589,plain,
! [X2,X0,X1] : add(n0,X2) = add(add(X1,inverse(X0)),X0),
inference(forward_subsumption_resolution,[],[f1488,f276]) ).
fof(f16268,plain,
! [X0,X1] :
( n0 != add(X0,inverse(X1))
| add(X0,X0) = add(X0,X1) ),
inference(superposition,[],[f1465,f1]) ).
fof(f16285,plain,
! [X1] :
( n0 != add(n0,inverse(X1))
| add(n0,X1) = add(n0,n0) ),
inference(superposition,[],[f1465,f276]) ).
fof(f16303,plain,
! [X0,X1] :
( n0 != n0
| add(add(X0,X1),X0) = add(add(X0,X1),add(X0,X1)) ),
inference(superposition,[],[f1465,f269]) ).
fof(f16314,plain,
! [X0,X1] : add(add(X0,X1),X0) = add(add(X0,X1),add(X0,X1)),
inference(trivial_inequality_removal,[],[f16303]) ).
fof(f16323,plain,
! [X0,X1] : add(X0,X1) = add(add(X0,X1),X0),
inference(forward_demodulation,[],[f16314,f1]) ).
fof(f16330,plain,
! [X1] : add(n0,X1) = add(n0,n0),
inference(forward_subsumption_resolution,[],[f16285,f276]) ).
fof(f16347,plain,
! [X0,X1] :
( n0 != add(X0,inverse(X1))
| add(X0,X1) = X0 ),
inference(forward_demodulation,[],[f16268,f1]) ).
fof(f16350,plain,
! [X1] : n0 = add(n0,X1),
inference(forward_demodulation,[],[f16330,f1]) ).
fof(f26314,plain,
! [X2,X0,X1] :
( n0 != add(add(n0,X1),inverse(X2))
| add(add(n0,X1),X2) = add(add(X0,X1),n0) ),
inference(superposition,[],[f3,f16350]) ).
fof(f26329,plain,
! [X2,X0,X1] :
( n0 != add(n0,inverse(X2))
| add(add(n0,X1),X2) = add(add(X0,X1),n0) ),
inference(forward_demodulation,[],[f26314,f16350]) ).
fof(f26332,plain,
! [X2,X0,X1] : add(add(n0,X1),X2) = add(add(X0,X1),n0),
inference(forward_subsumption_resolution,[],[f26329,f276]) ).
fof(f26334,plain,
! [X2,X0,X1] : add(n0,X2) = add(add(X0,X1),n0),
inference(forward_demodulation,[],[f26332,f16350]) ).
fof(f26336,plain,
! [X0,X1] : n0 = add(add(X0,X1),n0),
inference(forward_demodulation,[],[f26334,f16350]) ).
fof(f26338,plain,
! [X0] : n0 = add(X0,n0),
inference(superposition,[],[f26336,f1]) ).
fof(f26484,plain,
! [X0,X1] : n0 = add(add(X1,inverse(X0)),X0),
inference(forward_demodulation,[],[f1589,f16350]) ).
fof(f26489,plain,
! [X0] : n0 = add(inverse(X0),X0),
inference(superposition,[],[f26484,f1]) ).
fof(f26492,plain,
! [X0,X1] : n0 = add(add(inverse(X0),X1),X0),
inference(superposition,[],[f26484,f16323]) ).
fof(f26508,plain,
! [X2,X3,X0,X1] :
( n0 != add(add(n0,X2),inverse(X3))
| add(add(n0,X2),X3) = add(add(X1,X2),add(X0,inverse(X1))) ),
inference(superposition,[],[f3,f26484]) ).
fof(f26524,plain,
! [X2,X3,X0,X1] :
( n0 != add(n0,inverse(X3))
| add(add(n0,X2),X3) = add(add(X1,X2),add(X0,inverse(X1))) ),
inference(forward_demodulation,[],[f26508,f16350]) ).
fof(f26533,plain,
! [X2,X3,X0,X1] : add(add(n0,X2),X3) = add(add(X1,X2),add(X0,inverse(X1))),
inference(forward_subsumption_resolution,[],[f26524,f276]) ).
fof(f26538,plain,
! [X2,X3,X0,X1] : add(n0,X3) = add(add(X1,X2),add(X0,inverse(X1))),
inference(forward_demodulation,[],[f26533,f16350]) ).
fof(f26542,plain,
! [X2,X0,X1] : n0 = add(add(X1,X2),add(X0,inverse(X1))),
inference(forward_demodulation,[],[f26538,f16350]) ).
fof(f26581,plain,
! [X2,X0,X1] :
( n0 != add(n0,inverse(X2))
| add(n0,X2) = add(add(X1,X0),inverse(X0)) ),
inference(superposition,[],[f3,f26492]) ).
fof(f26604,plain,
! [X2,X0,X1] : add(n0,X2) = add(add(X1,X0),inverse(X0)),
inference(forward_subsumption_resolution,[],[f26581,f276]) ).
fof(f26610,plain,
! [X0,X1] : n0 = add(add(X1,X0),inverse(X0)),
inference(forward_demodulation,[],[f26604,f16350]) ).
fof(f26635,plain,
! [X0,X1] :
( n0 != n0
| add(add(X0,X1),X0) = add(add(X0,X1),X1) ),
inference(superposition,[],[f1465,f26610]) ).
fof(f26647,plain,
! [X2,X3,X0,X1] :
( n0 != add(add(n0,X2),inverse(X3))
| add(add(n0,X2),X3) = add(add(inverse(X1),X2),add(X0,X1)) ),
inference(superposition,[],[f3,f26610]) ).
fof(f26661,plain,
! [X0,X1] : add(add(X0,X1),X0) = add(add(X0,X1),X1),
inference(trivial_inequality_removal,[],[f26635]) ).
fof(f26663,plain,
! [X2,X3,X0,X1] :
( n0 != add(n0,inverse(X3))
| add(add(n0,X2),X3) = add(add(inverse(X1),X2),add(X0,X1)) ),
inference(forward_demodulation,[],[f26647,f16350]) ).
fof(f26670,plain,
! [X0,X1] : add(X0,X1) = add(add(X0,X1),X1),
inference(forward_demodulation,[],[f26661,f16323]) ).
fof(f26672,plain,
! [X2,X3,X0,X1] : add(add(n0,X2),X3) = add(add(inverse(X1),X2),add(X0,X1)),
inference(forward_subsumption_resolution,[],[f26663,f276]) ).
fof(f26678,plain,
! [X2,X3,X0,X1] : add(n0,X3) = add(add(inverse(X1),X2),add(X0,X1)),
inference(forward_demodulation,[],[f26672,f16350]) ).
fof(f26683,plain,
! [X2,X0,X1] : n0 = add(add(inverse(X1),X2),add(X0,X1)),
inference(forward_demodulation,[],[f26678,f16350]) ).
fof(f26747,plain,
! [X0,X1] : n0 = add(X0,add(X1,inverse(X0))),
inference(superposition,[],[f26542,f1]) ).
fof(f26773,plain,
! [X2,X0,X1] : n0 = add(add(X0,X2),add(inverse(X0),X1)),
inference(superposition,[],[f26542,f16323]) ).
fof(f26832,plain,
! [X0,X1] : n0 = add(X0,add(inverse(X0),X1)),
inference(superposition,[],[f26747,f16323]) ).
fof(f26976,plain,
! [X2,X3,X0,X1] :
( n0 != add(n0,inverse(X3))
| add(n0,X3) = add(add(X1,add(inverse(X0),X2)),X0) ),
inference(superposition,[],[f3,f26773]) ).
fof(f27003,plain,
! [X2,X3,X0,X1] : add(n0,X3) = add(add(X1,add(inverse(X0),X2)),X0),
inference(forward_subsumption_resolution,[],[f26976,f276]) ).
fof(f27009,plain,
! [X2,X0,X1] : n0 = add(add(X1,add(inverse(X0),X2)),X0),
inference(forward_demodulation,[],[f27003,f16350]) ).
fof(f27309,plain,
! [X0,X1] : n0 = add(inverse(X0),add(X1,X0)),
inference(superposition,[],[f26683,f1]) ).
fof(f28844,plain,
! [X0] :
( n0 != n0
| inverse(inverse(X0)) = add(inverse(inverse(X0)),X0) ),
inference(superposition,[],[f16347,f26489]) ).
fof(f28849,plain,
! [X0] : inverse(inverse(X0)) = add(inverse(inverse(X0)),X0),
inference(trivial_inequality_removal,[],[f28844]) ).
fof(f29552,plain,
n0 = inverse(inverse(n0)),
inference(superposition,[],[f28849,f26338]) ).
fof(f29597,plain,
! [X0] : n0 = add(X0,inverse(inverse(inverse(X0)))),
inference(superposition,[],[f26747,f28849]) ).
fof(f29625,plain,
! [X0] :
( n0 != add(X0,n0)
| add(X0,inverse(n0)) = X0 ),
inference(superposition,[],[f16347,f29552]) ).
fof(f29651,plain,
! [X0] : add(X0,inverse(n0)) = X0,
inference(forward_subsumption_resolution,[],[f29625,f26338]) ).
fof(f29824,plain,
! [X0,X1] :
( n0 != n0
| add(add(X0,X1),X0) = add(add(X1,add(X0,X1)),X0) ),
inference(superposition,[],[f1497,f162]) ).
fof(f29853,plain,
! [X0,X1] : add(add(X0,X1),X0) = add(add(X1,add(X0,X1)),X0),
inference(trivial_inequality_removal,[],[f29824]) ).
fof(f29858,plain,
! [X0,X1] : add(X0,X1) = add(add(X1,add(X0,X1)),X0),
inference(forward_demodulation,[],[f29853,f16323]) ).
fof(f30185,plain,
spl0_12,
inference(avatar_split_clause,[],[f29597,f431]) ).
fof(f30188,plain,
( ! [X0] :
( n0 != n0
| add(X0,inverse(inverse(X0))) = X0 )
| ~ spl0_12 ),
inference(superposition,[],[f16347,f432]) ).
fof(f30254,plain,
( ! [X0] : add(X0,inverse(inverse(X0))) = X0
| ~ spl0_12 ),
inference(trivial_inequality_removal,[],[f30188]) ).
fof(f32294,plain,
! [X0] : add(add(inverse(n0),X0),X0) = X0,
inference(superposition,[],[f29858,f29651]) ).
fof(f32300,plain,
! [X0,X1] : add(X0,X1) = add(add(X0,add(X0,X1)),add(X0,X1)),
inference(superposition,[],[f29858,f16323]) ).
fof(f32332,plain,
! [X0] : inverse(inverse(X0)) = add(add(X0,inverse(inverse(X0))),inverse(inverse(X0))),
inference(superposition,[],[f29858,f28849]) ).
fof(f32481,plain,
! [X0] : inverse(inverse(X0)) = add(X0,inverse(inverse(X0))),
inference(forward_demodulation,[],[f32332,f26670]) ).
fof(f32505,plain,
! [X0,X1] : add(X0,X1) = add(X0,add(X0,X1)),
inference(forward_demodulation,[],[f32300,f26670]) ).
fof(f32510,plain,
! [X0] : add(inverse(n0),X0) = X0,
inference(forward_demodulation,[],[f32294,f26670]) ).
fof(f32520,plain,
( ! [X0] : inverse(inverse(X0)) = X0
| ~ spl0_12 ),
inference(forward_demodulation,[],[f32481,f30254]) ).
fof(f32584,plain,
( ! [X0,X1] :
( n0 != add(X1,X0)
| add(X1,inverse(X0)) = X1 )
| ~ spl0_12 ),
inference(superposition,[],[f16347,f32520]) ).
fof(f34120,plain,
! [X0,X1] : add(X0,X1) = add(add(X1,add(X0,X1)),add(X0,X1)),
inference(superposition,[],[f32505,f29858]) ).
fof(f34247,plain,
! [X0,X1] : add(X0,X1) = add(X1,add(X0,X1)),
inference(forward_demodulation,[],[f34120,f26670]) ).
fof(f34449,plain,
! [X2,X0,X1] : add(add(X0,X1),X2) = add(add(X0,X2),add(X0,X1)),
inference(superposition,[],[f1561,f16323]) ).
fof(f34494,plain,
! [X0,X1] : add(X0,X1) = add(add(X1,X0),X0),
inference(superposition,[],[f1561,f16323]) ).
fof(f34585,plain,
! [X0,X1] : add(X0,X1) = add(add(X1,X0),X1),
inference(superposition,[],[f1561,f26670]) ).
fof(f34616,plain,
! [X0,X1] : add(add(X0,X0),X1) = add(X1,X0),
inference(superposition,[],[f26670,f1561]) ).
fof(f34647,plain,
! [X2,X0,X1] : n0 = add(add(add(X0,X1),X2),inverse(add(X2,X0))),
inference(superposition,[],[f162,f1561]) ).
fof(f34742,plain,
! [X2,X0,X1] : n0 = add(add(add(X0,X1),X2),inverse(add(X1,X2))),
inference(superposition,[],[f162,f1561]) ).
fof(f34886,plain,
! [X0,X1] : add(X0,X1) = add(X1,X0),
inference(forward_demodulation,[],[f34616,f1]) ).
fof(f35161,plain,
! [X2,X0,X1] : add(add(X0,X1),X2) = add(X0,add(X1,X2)),
inference(superposition,[],[f34886,f1561]) ).
fof(f35366,plain,
( b != add(inverse(add(a,inverse(b))),inverse(add(inverse(b),inverse(a))))
| spl0_3 ),
inference(superposition,[],[f17,f34886]) ).
fof(f35369,plain,
( add(b,a) != add(b,a)
| spl0_1 ),
inference(superposition,[],[f9,f34886]) ).
fof(f35504,plain,
( $false
| spl0_1 ),
inference(trivial_inequality_removal,[],[f35369]) ).
fof(f35505,plain,
spl0_1,
inference(avatar_contradiction_clause,[],[f35504]) ).
fof(f35648,plain,
! [X0,X1] : add(X0,X1) = add(X0,add(X1,X0)),
inference(forward_demodulation,[],[f34494,f34886]) ).
fof(f35656,plain,
! [X0,X1] : add(add(X1,X0),X0) = add(add(X1,X0),add(X0,X1)),
inference(superposition,[],[f35648,f35648]) ).
fof(f35670,plain,
! [X2,X0,X1] : add(X0,n0) = add(X0,add(X1,add(inverse(X0),X2))),
inference(superposition,[],[f35648,f27009]) ).
fof(f35675,plain,
! [X2,X0,X1] : add(X1,add(X2,X0)) = add(X1,add(add(X0,X1),X2)),
inference(superposition,[],[f35648,f1561]) ).
fof(f35743,plain,
! [X0,X1] : n0 = add(add(X0,X1),inverse(add(X1,X0))),
inference(superposition,[],[f26610,f35648]) ).
fof(f35852,plain,
! [X2,X0,X1] : n0 = add(X0,add(X1,add(inverse(X0),X2))),
inference(forward_demodulation,[],[f35670,f26338]) ).
fof(f35866,plain,
! [X0,X1] : add(X0,add(X1,X0)) = add(add(X1,X0),add(X0,X1)),
inference(forward_demodulation,[],[f35656,f34886]) ).
fof(f35888,plain,
! [X0,X1] : add(X1,X0) = add(add(X1,X0),add(X0,X1)),
inference(forward_demodulation,[],[f35866,f34247]) ).
fof(f35905,plain,
! [X0,X1] : add(X0,X1) = add(X1,add(X1,X0)),
inference(forward_demodulation,[],[f34585,f34886]) ).
fof(f37416,plain,
! [X2,X0,X1] :
( n0 != add(n0,inverse(X2))
| add(n0,X2) = add(add(X1,inverse(add(X1,X0))),X0) ),
inference(superposition,[],[f3,f35743]) ).
fof(f37510,plain,
! [X2,X0,X1] : add(n0,X2) = add(add(X1,inverse(add(X1,X0))),X0),
inference(forward_subsumption_resolution,[],[f37416,f276]) ).
fof(f37589,plain,
! [X2,X0,X1] : add(n0,X2) = add(X0,add(X1,inverse(add(X1,X0)))),
inference(forward_demodulation,[],[f37510,f34886]) ).
fof(f37613,plain,
! [X0,X1] : n0 = add(X0,add(X1,inverse(add(X1,X0)))),
inference(forward_demodulation,[],[f37589,f16350]) ).
fof(f38779,plain,
! [X0,X1] : n0 = add(X0,add(X1,inverse(add(X0,X1)))),
inference(superposition,[],[f37613,f34886]) ).
fof(f40058,plain,
( ! [X0,X1] :
( n0 != n0
| add(X0,inverse(add(X1,inverse(X0)))) = X0 )
| ~ spl0_12 ),
inference(superposition,[],[f32584,f26747]) ).
fof(f40061,plain,
( ! [X0,X1] :
( n0 != n0
| add(X0,inverse(add(X1,inverse(add(X0,X1))))) = X0 )
| ~ spl0_12 ),
inference(superposition,[],[f32584,f38779]) ).
fof(f40065,plain,
( ! [X2,X0,X1] :
( n0 != n0
| add(X0,inverse(add(X1,add(inverse(X0),X2)))) = X0 )
| ~ spl0_12 ),
inference(superposition,[],[f32584,f35852]) ).
fof(f40068,plain,
( ! [X0,X1] :
( n0 != n0
| add(X0,inverse(add(inverse(X0),X1))) = X0 )
| ~ spl0_12 ),
inference(superposition,[],[f32584,f26832]) ).
fof(f40092,plain,
( ! [X2,X0,X1] :
( n0 != n0
| add(X0,X1) = add(add(X0,X1),inverse(add(inverse(X0),X2))) )
| ~ spl0_12 ),
inference(superposition,[],[f32584,f26773]) ).
fof(f40111,plain,
( ! [X0,X1] :
( n0 != n0
| inverse(X0) = add(inverse(X0),inverse(add(X1,X0))) )
| ~ spl0_12 ),
inference(superposition,[],[f32584,f27309]) ).
fof(f40144,plain,
( ! [X0,X1] : inverse(X0) = add(inverse(X0),inverse(add(X1,X0)))
| ~ spl0_12 ),
inference(trivial_inequality_removal,[],[f40111]) ).
fof(f40162,plain,
( ! [X2,X0,X1] : add(X0,X1) = add(add(X0,X1),inverse(add(inverse(X0),X2)))
| ~ spl0_12 ),
inference(trivial_inequality_removal,[],[f40092]) ).
fof(f40178,plain,
( ! [X0,X1] : add(X0,inverse(add(inverse(X0),X1))) = X0
| ~ spl0_12 ),
inference(trivial_inequality_removal,[],[f40068]) ).
fof(f40181,plain,
( ! [X2,X0,X1] : add(X0,inverse(add(X1,add(inverse(X0),X2)))) = X0
| ~ spl0_12 ),
inference(trivial_inequality_removal,[],[f40065]) ).
fof(f40183,plain,
( ! [X0,X1] : add(X0,inverse(add(X1,inverse(add(X0,X1))))) = X0
| ~ spl0_12 ),
inference(trivial_inequality_removal,[],[f40061]) ).
fof(f40186,plain,
( ! [X0,X1] : add(X0,inverse(add(X1,inverse(X0)))) = X0
| ~ spl0_12 ),
inference(trivial_inequality_removal,[],[f40058]) ).
fof(f40956,plain,
( ! [X0,X1] : inverse(X0) = add(inverse(X0),inverse(add(X0,X1)))
| ~ spl0_12 ),
inference(superposition,[],[f40178,f32520]) ).
fof(f41249,plain,
( ! [X2,X0,X1] : add(X0,X2) = add(add(inverse(add(X1,inverse(X0))),X2),X0)
| ~ spl0_12 ),
inference(superposition,[],[f1561,f40186]) ).
fof(f41355,plain,
( ! [X2,X0,X1] : add(X0,X2) = add(X0,add(inverse(add(X1,inverse(X0))),X2))
| ~ spl0_12 ),
inference(forward_demodulation,[],[f41249,f34886]) ).
fof(f41407,plain,
( ! [X0,X1] : inverse(add(X1,X0)) = add(inverse(add(X1,X0)),inverse(add(X0,X1)))
| ~ spl0_12 ),
inference(superposition,[],[f40144,f35905]) ).
fof(f44149,plain,
! [X2,X0,X1] : add(X0,add(X1,X2)) = add(X1,add(X2,X0)),
inference(superposition,[],[f35161,f34886]) ).
fof(f58161,plain,
! [X2,X0,X1] : n0 = add(inverse(add(X2,X0)),add(add(X0,X1),X2)),
inference(forward_demodulation,[],[f34647,f34886]) ).
fof(f58162,plain,
! [X2,X0,X1] : n0 = add(X2,add(inverse(add(X2,X0)),add(X0,X1))),
inference(forward_demodulation,[],[f58161,f44149]) ).
fof(f58163,plain,
! [X2,X0,X1] : n0 = add(X2,add(X0,add(X1,inverse(add(X2,X0))))),
inference(forward_demodulation,[],[f58162,f44149]) ).
fof(f58166,plain,
! [X2,X0,X1] : n0 = add(inverse(add(X1,X2)),add(add(X0,X1),X2)),
inference(forward_demodulation,[],[f34742,f34886]) ).
fof(f58167,plain,
! [X2,X0,X1] : n0 = add(X2,add(inverse(add(X1,X2)),add(X0,X1))),
inference(forward_demodulation,[],[f58166,f44149]) ).
fof(f58168,plain,
! [X2,X0,X1] : n0 = add(X2,add(X1,add(inverse(add(X1,X2)),X0))),
inference(forward_demodulation,[],[f58167,f44149]) ).
fof(f58938,plain,
! [X2,X0,X1] : n0 = add(X0,add(X1,add(inverse(add(X0,X1)),X2))),
inference(superposition,[],[f58163,f16323]) ).
fof(f59545,plain,
! [X2,X0,X1] : n0 = add(add(X0,inverse(add(X0,X1))),add(X1,add(inverse(n0),X2))),
inference(superposition,[],[f58168,f37613]) ).
fof(f60022,plain,
! [X2,X0,X1] : n0 = add(X1,add(add(inverse(n0),X2),add(X0,inverse(add(X0,X1))))),
inference(forward_demodulation,[],[f59545,f44149]) ).
fof(f60121,plain,
! [X2,X0,X1] : n0 = add(X1,add(inverse(n0),add(X2,add(X0,inverse(add(X0,X1)))))),
inference(forward_demodulation,[],[f60022,f35161]) ).
fof(f60177,plain,
! [X2,X0,X1] : n0 = add(X1,add(X2,add(X0,inverse(add(X0,X1))))),
inference(forward_demodulation,[],[f60121,f32510]) ).
fof(f67101,plain,
! [X2,X0,X1] : add(add(X0,X1),X2) = add(X0,add(X1,add(X0,X2))),
inference(forward_demodulation,[],[f34449,f44149]) ).
fof(f67102,plain,
! [X2,X0,X1] : add(X0,add(X1,X2)) = add(X0,add(X1,add(X0,X2))),
inference(forward_demodulation,[],[f67101,f35161]) ).
fof(f67112,plain,
! [X2,X0,X1] : add(X0,add(X2,add(X0,X1))) = add(X0,add(X2,add(X1,X0))),
inference(superposition,[],[f67102,f35648]) ).
fof(f67177,plain,
! [X2,X0,X1] : add(add(X0,X1),add(X2,add(X0,X1))) = add(add(X0,X1),add(X2,add(X1,X0))),
inference(superposition,[],[f67102,f35888]) ).
fof(f67689,plain,
! [X2,X0,X1] : add(add(X0,X1),add(X2,add(X0,X1))) = add(X0,add(X1,add(X2,add(X1,X0)))),
inference(forward_demodulation,[],[f67177,f35161]) ).
fof(f67747,plain,
! [X2,X0,X1] : add(X0,add(X2,X1)) = add(X0,add(X2,add(X1,X0))),
inference(forward_demodulation,[],[f67112,f67102]) ).
fof(f67891,plain,
! [X2,X0,X1] : add(X0,add(X1,add(X2,X0))) = add(add(X0,X1),add(X2,add(X0,X1))),
inference(forward_demodulation,[],[f67689,f67102]) ).
fof(f68028,plain,
! [X2,X0,X1] : add(X0,add(X1,add(X2,X0))) = add(X2,add(X0,X1)),
inference(forward_demodulation,[],[f67891,f34247]) ).
fof(f68937,plain,
! [X2,X0,X1] : add(X1,add(X2,X0)) = add(X1,add(X0,add(X1,X2))),
inference(forward_demodulation,[],[f35675,f35161]) ).
fof(f70198,plain,
! [X2,X0,X1] : n0 = add(add(X0,add(X1,X2)),inverse(add(X1,add(X2,X0)))),
inference(superposition,[],[f26610,f67747]) ).
fof(f70381,plain,
! [X2,X0,X1] : n0 = add(X0,add(add(X1,X2),inverse(add(X1,add(X2,X0))))),
inference(forward_demodulation,[],[f70198,f35161]) ).
fof(f70615,plain,
! [X2,X0,X1] : n0 = add(X0,add(X1,add(X2,inverse(add(X1,add(X2,X0)))))),
inference(forward_demodulation,[],[f70381,f35161]) ).
fof(f71069,plain,
( ! [X2,X0,X1] : add(X0,add(inverse(add(X1,inverse(X0))),X2)) = add(X0,add(X2,X0))
| ~ spl0_12 ),
inference(superposition,[],[f68937,f40186]) ).
fof(f71684,plain,
( ! [X2,X0,X1] : add(X2,X0) = add(X0,add(inverse(add(X1,inverse(X0))),X2))
| ~ spl0_12 ),
inference(forward_demodulation,[],[f71069,f34247]) ).
fof(f72399,plain,
! [X2,X0,X1] : add(X1,add(X0,X2)) = add(X0,add(X2,add(X0,X1))),
inference(superposition,[],[f68028,f34886]) ).
fof(f78924,plain,
( ! [X2,X0,X1] : add(X0,X1) = add(X0,add(X1,inverse(add(inverse(X0),X2))))
| ~ spl0_12 ),
inference(forward_demodulation,[],[f40162,f35161]) ).
fof(f96287,plain,
! [X2,X3,X0,X1] : n0 = add(X1,add(add(X2,add(X1,X0)),add(X3,inverse(add(X0,add(X1,X2)))))),
inference(superposition,[],[f58163,f72399]) ).
fof(f96434,plain,
! [X2,X3,X0,X1] : n0 = add(X1,add(X2,add(add(X1,X0),add(X3,inverse(add(X0,add(X1,X2))))))),
inference(forward_demodulation,[],[f96287,f35161]) ).
fof(f96813,plain,
! [X2,X3,X0,X1] : n0 = add(X1,add(X2,add(X1,add(X0,add(X3,inverse(add(X0,add(X1,X2)))))))),
inference(forward_demodulation,[],[f96434,f35161]) ).
fof(f97112,plain,
! [X2,X3,X0,X1] : n0 = add(X1,add(X2,add(X0,add(X3,inverse(add(X0,add(X1,X2))))))),
inference(forward_demodulation,[],[f96813,f67102]) ).
fof(f127657,plain,
! [X2,X3,X0,X1] : n0 = add(add(X0,add(inverse(add(X1,X0)),X2)),add(X3,add(X1,inverse(add(X3,n0))))),
inference(superposition,[],[f70615,f58938]) ).
fof(f128617,plain,
! [X2,X3,X0,X1] : n0 = add(X0,add(add(inverse(add(X1,X0)),X2),add(X3,add(X1,inverse(add(X3,n0)))))),
inference(forward_demodulation,[],[f127657,f35161]) ).
fof(f128901,plain,
! [X2,X3,X0,X1] : n0 = add(X0,add(inverse(add(X1,X0)),add(X2,add(X3,add(X1,inverse(add(X3,n0))))))),
inference(forward_demodulation,[],[f128617,f35161]) ).
fof(f129049,plain,
! [X2,X3,X0,X1] : n0 = add(X0,add(inverse(add(X1,X0)),add(X2,add(X3,add(X1,inverse(n0)))))),
inference(forward_demodulation,[],[f128901,f26338]) ).
fof(f129135,plain,
! [X2,X3,X0,X1] : n0 = add(X0,add(inverse(add(X1,X0)),add(X2,add(X3,X1)))),
inference(forward_demodulation,[],[f129049,f29651]) ).
fof(f152618,plain,
! [X2,X3,X0,X1] :
( add(n0,inverse(add(X0,add(X1,add(X2,X0))))) != add(add(inverse(add(X0,add(X1,add(X2,X0)))),add(X1,add(X2,X0))),X3)
| n0 = add(add(inverse(add(X0,add(X1,add(X2,X0)))),add(X1,add(X2,X0))),inverse(X3)) ),
inference(superposition,[],[f26,f129135]) ).
fof(f153062,plain,
! [X2,X3,X0,X1] :
( add(n0,inverse(add(X0,add(X1,add(X2,X0))))) != add(inverse(add(X0,add(X1,add(X2,X0)))),add(add(X1,add(X2,X0)),X3))
| n0 = add(add(inverse(add(X0,add(X1,add(X2,X0)))),add(X1,add(X2,X0))),inverse(X3)) ),
inference(forward_demodulation,[],[f152618,f35161]) ).
fof(f153683,plain,
! [X2,X3,X0,X1] :
( add(add(X1,add(X2,X0)),add(X3,inverse(add(X0,add(X1,add(X2,X0)))))) != add(n0,inverse(add(X0,add(X1,add(X2,X0)))))
| n0 = add(add(inverse(add(X0,add(X1,add(X2,X0)))),add(X1,add(X2,X0))),inverse(X3)) ),
inference(forward_demodulation,[],[f153062,f44149]) ).
fof(f154129,plain,
! [X2,X3,X0,X1] :
( n0 != add(add(X1,add(X2,X0)),add(X3,inverse(add(X0,add(X1,add(X2,X0))))))
| n0 = add(add(inverse(add(X0,add(X1,add(X2,X0)))),add(X1,add(X2,X0))),inverse(X3)) ),
inference(forward_demodulation,[],[f153683,f276]) ).
fof(f154338,plain,
! [X2,X3,X0,X1] :
( n0 != add(X1,add(add(X2,X0),add(X3,inverse(add(X0,add(X1,add(X2,X0)))))))
| n0 = add(add(inverse(add(X0,add(X1,add(X2,X0)))),add(X1,add(X2,X0))),inverse(X3)) ),
inference(forward_demodulation,[],[f154129,f35161]) ).
fof(f154454,plain,
! [X2,X3,X0,X1] :
( n0 != add(X1,add(X2,add(X0,add(X3,inverse(add(X0,add(X1,add(X2,X0))))))))
| n0 = add(add(inverse(add(X0,add(X1,add(X2,X0)))),add(X1,add(X2,X0))),inverse(X3)) ),
inference(forward_demodulation,[],[f154338,f35161]) ).
fof(f154532,plain,
! [X2,X3,X0,X1] :
( n0 != add(X1,add(X2,add(X0,add(X3,inverse(add(X0,add(X1,X2)))))))
| n0 = add(add(inverse(add(X0,add(X1,add(X2,X0)))),add(X1,add(X2,X0))),inverse(X3)) ),
inference(forward_demodulation,[],[f154454,f67747]) ).
fof(f154589,plain,
! [X2,X3,X0,X1] :
( n0 = add(inverse(add(X0,add(X1,add(X2,X0)))),add(add(X1,add(X2,X0)),inverse(X3)))
| n0 != add(X1,add(X2,add(X0,add(X3,inverse(add(X0,add(X1,X2))))))) ),
inference(forward_demodulation,[],[f154532,f35161]) ).
fof(f154591,plain,
! [X2,X3,X0,X1] :
( n0 = add(add(X1,add(X2,X0)),add(inverse(X3),inverse(add(X0,add(X1,add(X2,X0))))))
| n0 != add(X1,add(X2,add(X0,add(X3,inverse(add(X0,add(X1,X2))))))) ),
inference(forward_demodulation,[],[f154589,f44149]) ).
fof(f154592,plain,
! [X2,X3,X0,X1] :
( n0 = add(X1,add(add(X2,X0),add(inverse(X3),inverse(add(X0,add(X1,add(X2,X0)))))))
| n0 != add(X1,add(X2,add(X0,add(X3,inverse(add(X0,add(X1,X2))))))) ),
inference(forward_demodulation,[],[f154591,f35161]) ).
fof(f154593,plain,
! [X2,X3,X0,X1] :
( n0 = add(X1,add(X2,add(X0,add(inverse(X3),inverse(add(X0,add(X1,add(X2,X0))))))))
| n0 != add(X1,add(X2,add(X0,add(X3,inverse(add(X0,add(X1,X2))))))) ),
inference(forward_demodulation,[],[f154592,f35161]) ).
fof(f154594,plain,
! [X2,X3,X0,X1] :
( n0 = add(X1,add(X2,add(X0,add(inverse(X3),inverse(add(X0,add(X1,X2)))))))
| n0 != add(X1,add(X2,add(X0,add(X3,inverse(add(X0,add(X1,X2))))))) ),
inference(forward_demodulation,[],[f154593,f67747]) ).
fof(f154595,plain,
! [X2,X3,X0,X1] : n0 = add(X1,add(X2,add(X0,add(inverse(X3),inverse(add(X0,add(X1,X2))))))),
inference(global_subsumption,[],[f154594,f97112]) ).
fof(f154597,plain,
( ! [X2,X3,X0,X1] : n0 = add(X1,add(X2,add(X3,add(X0,inverse(add(X3,add(X1,X2)))))))
| ~ spl0_12 ),
inference(superposition,[],[f154595,f32520]) ).
fof(f158800,plain,
( ! [X2,X3,X0,X1] : n0 = add(X1,add(X0,add(X2,add(X3,inverse(add(X2,add(X0,X1)))))))
| ~ spl0_12 ),
inference(superposition,[],[f154597,f34886]) ).
fof(f160999,plain,
( ! [X2,X3,X0,X1] : n0 = add(add(X0,inverse(add(X0,X1))),add(X2,add(X1,add(X3,inverse(n0)))))
| ~ spl0_12 ),
inference(superposition,[],[f158800,f60177]) ).
fof(f161982,plain,
( ! [X2,X3,X0,X1] : n0 = add(X0,add(inverse(add(X0,X1)),add(X2,add(X1,add(X3,inverse(n0))))))
| ~ spl0_12 ),
inference(forward_demodulation,[],[f160999,f35161]) ).
fof(f162414,plain,
( ! [X2,X3,X0,X1] : n0 = add(X0,add(inverse(add(X0,X1)),add(X2,add(X1,X3))))
| ~ spl0_12 ),
inference(forward_demodulation,[],[f161982,f29651]) ).
fof(f163699,plain,
( ! [X2,X3,X0,X1] :
( n0 != n0
| add(X0,inverse(add(inverse(add(X0,X1)),add(X2,add(X1,X3))))) = X0 )
| ~ spl0_12 ),
inference(superposition,[],[f32584,f162414]) ).
fof(f163880,plain,
( ! [X2,X3,X0,X1] : add(X0,inverse(add(inverse(add(X0,X1)),add(X2,add(X1,X3))))) = X0
| ~ spl0_12 ),
inference(trivial_inequality_removal,[],[f163699]) ).
fof(f168593,plain,
( ! [X2,X0,X1] : inverse(add(add(X0,add(X1,X2)),X1)) = add(inverse(add(add(X0,add(X1,X2)),X1)),inverse(add(X0,add(X1,X2))))
| ~ spl0_12 ),
inference(superposition,[],[f40183,f163880]) ).
fof(f168987,plain,
( ! [X2,X0,X1] : inverse(add(add(X0,add(X1,X2)),X1)) = add(inverse(add(X0,add(X1,X2))),inverse(add(add(X0,add(X1,X2)),X1)))
| ~ spl0_12 ),
inference(forward_demodulation,[],[f168593,f34886]) ).
fof(f169503,plain,
( ! [X2,X0,X1] : inverse(add(X0,add(X1,X2))) = inverse(add(add(X0,add(X1,X2)),X1))
| ~ spl0_12 ),
inference(forward_demodulation,[],[f168987,f40956]) ).
fof(f169787,plain,
( ! [X2,X0,X1] : inverse(add(X0,add(X1,X2))) = inverse(add(X1,add(X0,add(X1,X2))))
| ~ spl0_12 ),
inference(forward_demodulation,[],[f169503,f34886]) ).
fof(f169899,plain,
( ! [X2,X0,X1] : inverse(add(X0,add(X1,X2))) = inverse(add(X1,add(X0,X2)))
| ~ spl0_12 ),
inference(forward_demodulation,[],[f169787,f67102]) ).
fof(f170474,plain,
( ! [X2,X0,X1] : inverse(add(X0,X1)) = inverse(add(X1,add(X0,inverse(add(inverse(X0),X2)))))
| ~ spl0_12 ),
inference(superposition,[],[f169899,f78924]) ).
fof(f171154,plain,
( ! [X0,X1] : inverse(add(X0,X1)) = inverse(add(X1,X0))
| ~ spl0_12 ),
inference(forward_demodulation,[],[f170474,f40178]) ).
fof(f225755,plain,
( ! [X2,X0,X1] : inverse(add(add(inverse(add(X2,inverse(X1))),X0),X1)) = add(inverse(add(add(inverse(add(X2,inverse(X1))),X0),X1)),inverse(add(X0,X1)))
| ~ spl0_12 ),
inference(superposition,[],[f41407,f71684]) ).
fof(f226394,plain,
( ! [X2,X0,X1] : inverse(add(add(inverse(add(X2,inverse(X1))),X0),X1)) = add(inverse(add(X0,X1)),inverse(add(add(inverse(add(X2,inverse(X1))),X0),X1)))
| ~ spl0_12 ),
inference(forward_demodulation,[],[f225755,f34886]) ).
fof(f226734,plain,
( ! [X2,X0,X1] : inverse(add(X1,add(inverse(add(X2,inverse(X1))),X0))) = add(inverse(add(X0,X1)),inverse(add(X1,add(inverse(add(X2,inverse(X1))),X0))))
| ~ spl0_12 ),
inference(forward_demodulation,[],[f226394,f171154]) ).
fof(f226989,plain,
( ! [X0,X1] : inverse(add(X1,X0)) = add(inverse(add(X0,X1)),inverse(add(X1,X0)))
| ~ spl0_12 ),
inference(forward_demodulation,[],[f226734,f41355]) ).
fof(f230536,plain,
( ! [X2,X0,X1] : add(X1,X0) = add(add(X1,X0),inverse(add(X2,inverse(add(X0,X1)))))
| ~ spl0_12 ),
inference(superposition,[],[f40181,f226989]) ).
fof(f230957,plain,
( ! [X2,X0,X1] : add(X1,X0) = add(X1,add(X0,inverse(add(X2,inverse(add(X0,X1))))))
| ~ spl0_12 ),
inference(forward_demodulation,[],[f230536,f35161]) ).
fof(f239418,plain,
( ! [X0,X1] : add(inverse(add(X0,X1)),X1) = add(inverse(add(X0,X1)),add(X1,inverse(X0)))
| ~ spl0_12 ),
inference(superposition,[],[f230957,f40183]) ).
fof(f240185,plain,
( ! [X0,X1] : add(inverse(add(X0,X1)),X1) = add(X1,add(inverse(X0),inverse(add(X0,X1))))
| ~ spl0_12 ),
inference(forward_demodulation,[],[f239418,f44149]) ).
fof(f240568,plain,
( ! [X0,X1] : add(X1,inverse(X0)) = add(inverse(add(X0,X1)),X1)
| ~ spl0_12 ),
inference(forward_demodulation,[],[f240185,f40956]) ).
fof(f240809,plain,
( ! [X0,X1] : add(X1,inverse(X0)) = add(X1,inverse(add(X0,X1)))
| ~ spl0_12 ),
inference(forward_demodulation,[],[f240568,f34886]) ).
fof(f241197,plain,
( ! [X0,X1] : add(inverse(add(X1,X0)),inverse(X0)) = add(inverse(add(X1,X0)),inverse(add(X0,inverse(X1))))
| ~ spl0_12 ),
inference(superposition,[],[f240809,f240809]) ).
fof(f241947,plain,
( ! [X0,X1] : add(inverse(X0),inverse(add(X1,X0))) = add(inverse(add(X1,X0)),inverse(add(X0,inverse(X1))))
| ~ spl0_12 ),
inference(forward_demodulation,[],[f241197,f34886]) ).
fof(f242244,plain,
( ! [X0,X1] : inverse(X0) = add(inverse(add(X1,X0)),inverse(add(X0,inverse(X1))))
| ~ spl0_12 ),
inference(forward_demodulation,[],[f241947,f40144]) ).
fof(f263717,plain,
( b != inverse(inverse(b))
| spl0_3
| ~ spl0_12 ),
inference(superposition,[],[f35366,f242244]) ).
fof(f264293,plain,
( $false
| spl0_3
| ~ spl0_12 ),
inference(forward_subsumption_resolution,[],[f263717,f32520]) ).
fof(f264294,plain,
( spl0_3
| ~ spl0_12 ),
inference(avatar_contradiction_clause,[],[f264293]) ).
fof(f265409,plain,
( $false
| spl0_2 ),
inference(forward_subsumption_resolution,[],[f13,f35161]) ).
fof(f265410,plain,
spl0_2,
inference(avatar_contradiction_clause,[],[f265409]) ).
cnf(s6,plain,
( ~ spl0_1
| ~ spl0_2
| ~ spl0_3 ),
inference(sat_conversion,[],[f18]) ).
cnf(s5398,plain,
spl0_12,
inference(sat_conversion,[],[f30185]) ).
cnf(s5980,plain,
spl0_1,
inference(sat_conversion,[],[f35505]) ).
cnf(s36253,plain,
( spl0_3
| ~ spl0_12 ),
inference(sat_conversion,[],[f264294]) ).
cnf(s36498,plain,
spl0_2,
inference(sat_conversion,[],[f265410]) ).
cnf(s36500,plain,
spl0_3,
inference(rat,[],[s36253,s5398]) ).
cnf(s36596,plain,
$false,
inference(rat,[],[s6,s36500,s36498,s5980]) ).
fof(f265413,plain,
$false,
inference(avatar_sat_refutation,[],[s36596]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : BOO020-1 : TPTP v9.3.1. Released v2.2.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.19 % Computer : n009.cluster.edu
% 0.08/0.19 % Model : x86_64 x86_64
% 0.08/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.19 % Memory : 8046.5625MB
% 0.08/0.19 % OS : Linux 6.8.0-71-generic
% 0.08/0.19 % CPULimit : 300
% 0.08/0.19 % WCLimit : 300
% 0.08/0.19 % DateTime : Mon Sep 28 21:04:30 UTC 2026
% 0.08/0.20 % CPUTime :
% 0.08/0.20 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.23 Running first-order model finding
% 0.08/0.23 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
% 13.92/2.23 % (3477345)Will run a generic schedule for satisfiability detection.
% 13.92/2.23 % (3477354)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1805705273:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 13.92/2.23 % (3477351)% WARNING: option uhcvi not known.
% 13.92/2.23 % (3477350)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=202452368_2999 on theBenchmark for (2999ds/0Mi)
% 13.92/2.23 % (3477351)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3808768814:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 13.92/2.23 % (3477352)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4090682895:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 13.92/2.23 % (3477353)dis+10_1_sil=32000:sp=arity:random_seed=4152794634:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 13.92/2.23 % (3477355)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3631703589:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 13.92/2.23 % (3477356)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1116254892:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 13.92/2.23 % TRYING [1]
% 13.92/2.23 % TRYING [2]
% 13.92/2.23 % TRYING [3]
% 13.92/2.23 % TRYING [4]
% 13.92/2.23 % (3477354)Instruction limit reached!
% 13.92/2.23 % (3477354)------------------------------
% 13.92/2.23 % (3477354)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.92/2.23 % (3477354)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.92/2.23 % (3477354)CaDiCaL version: 2.1.3
% 13.92/2.23 % (3477354)Termination reason: Instruction limit
% 13.92/2.23 % (3477354)Termination phase: Saturation
% 13.92/2.23 % (3477354)Time elapsed: 0.034 s
% 13.92/2.23 % (3477354)Peak memory usage: 12 MB
% 13.92/2.23 % (3477354)Instructions burned: 119 (million)
% 13.92/2.23 % TRYING [5]
% 13.92/2.23 % (3477364)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1655271062:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 13.92/2.23 % TRYING [1]
% 13.92/2.23 % TRYING [2]
% 13.92/2.23 % TRYING [3]
% 13.92/2.23 % TRYING [4]
% 13.92/2.23 % (3477353)Instruction limit reached!
% 13.92/2.23 % (3477353)------------------------------
% 13.92/2.23 % (3477353)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.92/2.23 % (3477353)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.92/2.23 % (3477353)CaDiCaL version: 2.1.3
% 13.92/2.23 % (3477353)Termination reason: Instruction limit
% 13.92/2.23 % (3477353)Termination phase: Saturation
% 13.92/2.23 % (3477353)Time elapsed: 0.057 s
% 13.92/2.23 % (3477353)Peak memory usage: 12 MB
% 13.92/2.23 % (3477353)Instructions burned: 105 (million)
% 13.92/2.23 % TRYING [5]
% 13.92/2.23 % (3477355)Instruction limit reached!
% 13.92/2.23 % (3477355)------------------------------
% 13.92/2.23 % (3477355)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.92/2.23 % (3477355)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.92/2.23 % (3477355)CaDiCaL version: 2.1.3
% 13.92/2.23 % (3477355)Termination reason: Instruction limit
% 13.92/2.23 % (3477355)Termination phase: Saturation
% 13.92/2.23 % (3477355)Time elapsed: 0.072 s
% 13.92/2.23 % (3477355)Peak memory usage: 12 MB
% 13.92/2.23 % (3477355)Instructions burned: 133 (million)
% 13.92/2.23 % (3477366)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=340826944:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 13.92/2.23 % (3477367)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=3919674561:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 13.92/2.23 % (3477356)Instruction limit reached!
% 13.92/2.23 % (3477356)------------------------------
% 13.92/2.23 % (3477356)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.92/2.23 % (3477356)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.92/2.23 % (3477356)CaDiCaL version: 2.1.3
% 13.92/2.23 % (3477356)Termination reason: Instruction limit
% 13.92/2.23 % (3477356)Termination phase: Saturation
% 13.92/2.23 % (3477356)Time elapsed: 0.097 s
% 13.92/2.23 % (3477356)Peak memory usage: 12 MB
% 13.92/2.23 % (3477356)Instructions burned: 159 (million)
% 13.92/2.23 % (3477370)ott-21_1_sil=16000:fs=off:random_seed=239171916:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 13.92/2.23 % TRYING [6]
% 13.92/2.23 % TRYING [6]
% 13.92/2.23 % (3477366)Instruction limit reached!
% 13.92/2.23 % (3477366)------------------------------
% 13.92/2.23 % (3477366)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.79/5.80 % (3477366)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.79/5.80 % (3477366)CaDiCaL version: 2.1.3
% 38.79/5.80 % (3477366)Termination reason: Instruction limit
% 38.79/5.80 % (3477366)Termination phase: Saturation
% 38.79/5.80 % (3477366)Time elapsed: 0.082 s
% 38.79/5.80 % (3477366)Peak memory usage: 12 MB
% 38.79/5.80 % (3477366)Instructions burned: 131 (million)
% 38.79/5.80 % (3477372)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=4131506884:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 38.79/5.80 % (3477364)Instruction limit reached!
% 38.79/5.80 % (3477364)------------------------------
% 38.79/5.80 % (3477364)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.79/5.80 % (3477364)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.79/5.80 % (3477364)CaDiCaL version: 2.1.3
% 38.79/5.80 % (3477364)Termination reason: Instruction limit
% 38.79/5.80 % (3477364)Termination phase: Finite model building constraint generation
% 38.79/5.80 % (3477364)Time elapsed: 0.149 s
% 38.79/5.80 % (3477364)Peak memory usage: 28 MB
% 38.79/5.80 % (3477364)Instructions burned: 715 (million)
% 38.79/5.80 % (3477374)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3251078539:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 38.79/5.80 % TRYING [1]
% 38.79/5.80 % TRYING [2]
% 38.79/5.80 % TRYING [3]
% 38.79/5.80 % (3477370)Instruction limit reached!
% 38.79/5.80 % (3477370)------------------------------
% 38.79/5.80 % (3477370)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.79/5.80 % (3477370)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.79/5.80 % (3477370)CaDiCaL version: 2.1.3
% 38.79/5.80 % (3477370)Termination reason: Instruction limit
% 38.79/5.80 % (3477370)Termination phase: Saturation
% 38.79/5.80 % (3477370)Time elapsed: 0.088 s
% 38.79/5.80 % (3477370)Peak memory usage: 11 MB
% 38.79/5.80 % (3477370)Instructions burned: 180 (million)
% 38.79/5.80 % TRYING [4]
% 38.79/5.80 % (3477376)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2047717462:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 38.79/5.80 % TRYING [5]
% 38.79/5.80 % TRYING [6]
% 38.79/5.80 % (3477374)Instruction limit reached!
% 38.79/5.80 % (3477374)------------------------------
% 38.79/5.80 % (3477374)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.79/5.80 % (3477374)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.79/5.80 % (3477374)CaDiCaL version: 2.1.3
% 38.79/5.80 % (3477374)Termination reason: Instruction limit
% 38.79/5.80 % (3477374)Termination phase: Finite model building constraint generation
% 38.79/5.80 % (3477374)Time elapsed: 0.166 s
% 38.79/5.80 % (3477374)Peak memory usage: 22 MB
% 38.79/5.80 % (3477374)Instructions burned: 867 (million)
% 38.79/5.80 % (3477378)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=894099152:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 38.79/5.80 % TRYING [7]
% 38.79/5.80 % TRYING [14]
% 38.79/5.80 % (3477372)Instruction limit reached!
% 38.79/5.80 % (3477372)------------------------------
% 38.79/5.80 % (3477372)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.79/5.80 % (3477372)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.79/5.80 % (3477372)CaDiCaL version: 2.1.3
% 38.79/5.80 % (3477372)Termination reason: Instruction limit
% 38.79/5.80 % (3477372)Termination phase: Saturation
% 38.79/5.80 % (3477372)Time elapsed: 0.269 s
% 38.79/5.80 % (3477372)Peak memory usage: 13 MB
% 38.79/5.80 % (3477372)Instructions burned: 477 (million)
% 38.79/5.80 % (3477367)Instruction limit reached!
% 38.79/5.80 % (3477367)------------------------------
% 38.79/5.80 % (3477367)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.79/5.80 % (3477367)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.79/5.80 % (3477367)CaDiCaL version: 2.1.3
% 38.79/5.80 % (3477367)Termination reason: Instruction limit
% 38.79/5.80 % (3477367)Termination phase: Saturation
% 38.79/5.80 % (3477367)Time elapsed: 0.361 s
% 38.79/5.80 % (3477367)Peak memory usage: 16 MB
% 38.79/5.80 % (3477367)Instructions burned: 685 (million)
% 38.79/5.80 % (3477380)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=2434231000:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2995 on theBenchmark for (2995ds/692Mi)
% 38.79/5.80 % (3477381)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=581690126:i=879:kws=inv_precedence:fsr=off_2995 on theBenchmark for (2995ds/879Mi)
% 64.20/9.39 % (3477378)Instruction limit reached!
% 64.20/9.39 % (3477378)------------------------------
% 64.20/9.39 % (3477378)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 64.20/9.39 % (3477378)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.20/9.39 % (3477378)CaDiCaL version: 2.1.3
% 64.20/9.39 % (3477378)Termination reason: Instruction limit
% 64.20/9.39 % (3477378)Termination phase: Finite model building constraint generation
% 64.20/9.39 % (3477378)Time elapsed: 0.188 s
% 64.20/9.39 % (3477378)Peak memory usage: 81 MB
% 64.20/9.39 % (3477378)Instructions burned: 895 (million)
% 64.20/9.39 % (3477384)fmb+10_1_sil=64000:random_seed=1247371676:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi)
% 64.20/9.39 % TRYING [1]
% 64.20/9.39 % TRYING [2]
% 64.20/9.39 % TRYING [3]
% 64.20/9.39 % TRYING [4]
% 64.20/9.39 % TRYING [5]
% 64.20/9.39 % TRYING [6]
% 64.20/9.39 % (3477376)Instruction limit reached!
% 64.20/9.39 % (3477376)------------------------------
% 64.20/9.39 % (3477376)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 64.20/9.39 % (3477376)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.20/9.39 % (3477376)CaDiCaL version: 2.1.3
% 64.20/9.39 % (3477376)Termination reason: Instruction limit
% 64.20/9.39 % (3477376)Termination phase: Saturation
% 64.20/9.39 % (3477376)Time elapsed: 0.620 s
% 64.20/9.39 % (3477376)Peak memory usage: 22 MB
% 64.20/9.39 % (3477376)Instructions burned: 1180 (million)
% 64.20/9.39 % (3477380)Instruction limit reached!
% 64.20/9.39 % (3477380)------------------------------
% 64.20/9.39 % (3477380)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 64.20/9.39 % (3477380)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.20/9.39 % (3477380)CaDiCaL version: 2.1.3
% 64.20/9.39 % (3477380)Termination reason: Instruction limit
% 64.20/9.39 % (3477380)Termination phase: Saturation
% 64.20/9.39 % (3477380)Time elapsed: 0.382 s
% 64.20/9.39 % (3477380)Peak memory usage: 15 MB
% 64.20/9.39 % (3477380)Instructions burned: 693 (million)
% 64.20/9.39 % (3477386)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2360150084:i=9515:nm=5_2991 on theBenchmark for (2991ds/9515Mi)
% 64.20/9.39 % TRYING [20]
% 64.20/9.39 % (3477387)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1031134734:fmbsr=1.7:i=920_2991 on theBenchmark for (2991ds/920Mi)
% 64.20/9.39 % TRYING [8]
% 64.20/9.39 % (3477381)Instruction limit reached!
% 64.20/9.39 % (3477381)------------------------------
% 64.20/9.39 % (3477381)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 64.20/9.39 % (3477381)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.20/9.39 % (3477381)CaDiCaL version: 2.1.3
% 64.20/9.39 % (3477381)Termination reason: Instruction limit
% 64.20/9.39 % (3477381)Termination phase: Saturation
% 64.20/9.39 % (3477381)Time elapsed: 0.472 s
% 64.20/9.39 % (3477381)Peak memory usage: 17 MB
% 64.20/9.39 % (3477381)Instructions burned: 881 (million)
% 64.20/9.39 % (3477390)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=913882292:i=5131_2990 on theBenchmark for (2990ds/5131Mi)
% 64.20/9.39 % TRYING [7]
% 64.20/9.39 % (3477387)Instruction limit reached!
% 64.20/9.39 % (3477387)------------------------------
% 64.20/9.39 % (3477387)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 64.20/9.39 % (3477387)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.20/9.39 % (3477387)CaDiCaL version: 2.1.3
% 64.20/9.39 % (3477387)Termination reason: Instruction limit
% 64.20/9.39 % (3477387)Termination phase: Finite model building constraint generation
% 64.20/9.39 % (3477387)Time elapsed: 0.323 s
% 64.20/9.39 % (3477387)Peak memory usage: 67 MB
% 64.20/9.39 % (3477387)Instructions burned: 921 (million)
% 64.20/9.39 % (3477392)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=211671734:i=1472:ins=7:fdi=8:gsp=on_2987 on theBenchmark for (2987ds/1472Mi)
% 64.20/9.39 % TRYING [8]
% 64.20/9.39 % (3477392)Instruction limit reached!
% 64.20/9.39 % (3477392)------------------------------
% 64.20/9.39 % (3477392)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 64.20/9.39 % (3477392)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.20/9.39 % (3477392)CaDiCaL version: 2.1.3
% 64.20/9.39 % (3477392)Termination reason: Instruction limit
% 64.20/9.39 % (3477392)Termination phase: Saturation
% 64.20/9.39 % (3477392)Time elapsed: 0.717 s
% 64.20/9.39 % (3477392)Peak memory usage: 25 MB
% 64.20/9.39 % (3477392)Instructions burned: 1473 (million)
% 64.20/9.39 % (3477394)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1664921270:i=6324_2980 on theBenchmark for (2980ds/6324Mi)
% 64.20/9.39 % TRYING [77]
% 64.20/9.39 % TRYING [8]
% 64.20/9.39 % (3477390)Instruction limit reached!
% 64.20/9.39 % (3477390)------------------------------
% 64.20/9.39 % (3477390)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 64.20/9.39 % (3477390)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.20/9.39 % (3477390)CaDiCaL version: 2.1.3
% 64.20/9.39 % (3477390)Termination reason: Instruction limit
% 64.20/9.39 % (3477390)Termination phase: Saturation
% 64.20/9.39 % (3477390)Time elapsed: 2.647 s
% 64.20/9.39 % (3477390)Peak memory usage: 53 MB
% 64.20/9.39 % (3477390)Instructions burned: 5131 (million)
% 64.20/9.39 % (3477396)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2852340530:fmbsr=2.30978:i=2174_2963 on theBenchmark for (2963ds/2174Mi)
% 64.20/9.39 % TRYING [16]
% 64.20/9.39 % (3477386)Instruction limit reached!
% 64.20/9.39 % (3477386)------------------------------
% 64.20/9.39 % (3477386)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 64.20/9.39 % (3477386)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.20/9.39 % (3477386)CaDiCaL version: 2.1.3
% 64.20/9.39 % (3477386)Termination reason: Instruction limit
% 64.20/9.39 % (3477386)Termination phase: Finite model building constraint generation
% 64.20/9.39 % (3477386)Time elapsed: 3.437 s
% 64.20/9.39 % (3477386)Peak memory usage: 644 MB
% 64.20/9.39 % (3477386)Instructions burned: 9518 (million)
% 64.20/9.39 % (3477394)Instruction limit reached!
% 64.20/9.39 % (3477394)------------------------------
% 64.20/9.39 % (3477394)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 64.20/9.39 % (3477394)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.20/9.39 % (3477394)CaDiCaL version: 2.1.3
% 64.20/9.39 % (3477394)Termination reason: Instruction limit
% 64.20/9.39 % (3477394)Termination phase: Finite model building constraint generation
% 64.20/9.39 % (3477394)Time elapsed: 2.352 s
% 64.20/9.39 % (3477394)Peak memory usage: 521 MB
% 64.20/9.39 % (3477394)Instructions burned: 6327 (million)
% 64.20/9.39 % (3477396)Instruction limit reached!
% 64.20/9.39 % (3477396)------------------------------
% 64.20/9.39 % (3477396)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 64.20/9.39 % (3477396)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.20/9.39 % (3477396)CaDiCaL version: 2.1.3
% 64.20/9.39 % (3477396)Termination reason: Instruction limit
% 64.20/9.39 % (3477396)Termination phase: Finite model building constraint generation
% 64.20/9.39 % (3477396)Time elapsed: 0.731 s
% 64.20/9.39 % (3477396)Peak memory usage: 133 MB
% 64.20/9.39 % (3477396)Instructions burned: 2175 (million)
% 64.20/9.39 % (3477398)ott-2_1_sil=16000:newcnf=on:random_seed=3405590306:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2955 on theBenchmark for (2955ds/869Mi)
% 64.20/9.39 % (3477399)ott+10_1_sil=32000:tgt=ground:random_seed=2669599531:i=5114:av=off_2955 on theBenchmark for (2955ds/5114Mi)
% 64.20/9.39 % (3477400)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2761457195:i=54282_2955 on theBenchmark for (2955ds/54282Mi)
% 64.20/9.39 % TRYING [1]
% 64.20/9.39 % TRYING [2]
% 64.20/9.39 % TRYING [3]
% 64.20/9.39 % TRYING [4]
% 64.20/9.39 % TRYING [5]
% 64.20/9.39 % TRYING [6]
% 64.20/9.39 % TRYING [7]
% 64.20/9.39 % TRYING [9]
% 64.20/9.39 % (3477398)Instruction limit reached!
% 64.20/9.39 % (3477398)------------------------------
% 64.20/9.39 % (3477398)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 64.20/9.39 % (3477398)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.20/9.39 % (3477398)CaDiCaL version: 2.1.3
% 64.20/9.39 % (3477398)Termination reason: Instruction limit
% 64.20/9.39 % (3477398)Termination phase: Saturation
% 64.20/9.39 % (3477398)Time elapsed: 0.477 s
% 64.20/9.39 % (3477398)Peak memory usage: 15 MB
% 64.20/9.39 % (3477398)Instructions burned: 871 (million)
% 64.20/9.39 % (3477404)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2024155873:i=3512:aac=none_2950 on theBenchmark for (2950ds/3512Mi)
% 64.20/9.39 % (3477384)Instruction limit reached!
% 64.20/9.39 % (3477384)------------------------------
% 64.20/9.39 % (3477384)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 64.20/9.39 % (3477384)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.20/9.39 % (3477384)CaDiCaL version: 2.1.3
% 64.20/9.39 % (3477384)Termination reason: Instruction limit
% 64.20/9.39 % (3477384)Termination phase: Finite model building constraint generation
% 64.20/9.39 % (3477384)Time elapsed: 4.948 s
% 64.20/9.39 % (3477384)Peak memory usage: 225 MB
% 64.20/9.39 % (3477384)Instructions burned: 22062 (million)
% 64.20/9.39 % (3477406)dis+21_1_sil=32000:sas=cadical:random_seed=1953027454:i=3773:amm=off_2944 on theBenchmark for (2944ds/3773Mi)
% 64.20/9.39 % TRYING [8]
% 64.20/9.39 % (3477406)Instruction limit reached!
% 64.20/9.39 % (3477406)------------------------------
% 64.20/9.39 % (3477406)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 64.20/9.39 % (3477406)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.20/9.39 % (3477406)CaDiCaL version: 2.1.3
% 64.20/9.39 % (3477406)Termination reason: Instruction limit
% 64.20/9.39 % (3477406)Termination phase: Saturation
% 64.20/9.39 % (3477406)Time elapsed: 1.038 s
% 64.20/9.39 % (3477406)Peak memory usage: 29 MB
% 64.20/9.39 % (3477406)Instructions burned: 3778 (million)
% 64.20/9.39 % (3477408)ott+11_1_sil=16000:gs=on:random_seed=681396184:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2933 on theBenchmark for (2933ds/2251Mi)
% 64.20/9.39 % (3477404)Instruction limit reached!
% 64.20/9.39 % (3477404)------------------------------
% 64.20/9.39 % (3477404)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 64.20/9.39 % (3477404)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.20/9.39 % (3477404)CaDiCaL version: 2.1.3
% 64.20/9.39 % (3477404)Termination reason: Instruction limit
% 64.20/9.39 % (3477404)Termination phase: Saturation
% 64.20/9.39 % (3477404)Time elapsed: 1.828 s
% 64.20/9.39 % (3477404)Peak memory usage: 29 MB
% 64.20/9.39 % (3477404)Instructions burned: 3514 (million)
% 64.20/9.39 % (3477410)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2448992045:fmbsr=1.6:i=67534_2932 on theBenchmark for (2932ds/67534Mi)
% 64.20/9.39 % TRYING [9]
% 64.20/9.39 % TRYING [7]
% 64.20/9.39 % (3477399)Instruction limit reached!
% 64.20/9.39 % (3477399)------------------------------
% 64.20/9.39 % (3477399)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 64.20/9.39 % (3477399)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.20/9.39 % (3477399)CaDiCaL version: 2.1.3
% 64.20/9.39 % (3477399)Termination reason: Instruction limit
% 64.20/9.39 % (3477399)Termination phase: Saturation
% 64.20/9.39 % (3477399)Time elapsed: 2.759 s
% 64.20/9.39 % (3477399)Peak memory usage: 50 MB
% 64.20/9.39 % (3477399)Instructions burned: 5115 (million)
% 64.20/9.39 % (3477412)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=4271995463:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2927 on theBenchmark for (2927ds/4591Mi)
% 64.20/9.39 % (3477408)Instruction limit reached!
% 64.20/9.39 % (3477408)------------------------------
% 64.20/9.39 % (3477408)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 64.20/9.39 % (3477408)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.20/9.39 % (3477408)CaDiCaL version: 2.1.3
% 64.20/9.39 % (3477408)Termination reason: Instruction limit
% 64.20/9.39 % (3477408)Termination phase: Saturation
% 64.20/9.39 % (3477408)Time elapsed: 0.607 s
% 64.20/9.39 % (3477408)Peak memory usage: 21 MB
% 64.20/9.39 % (3477408)Instructions burned: 2251 (million)
% 64.20/9.39 % (3477414)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=1620872365:i=29340_2927 on theBenchmark for (2927ds/29340Mi)
% 64.20/9.39 % (3477412)Instruction limit reached!
% 64.20/9.39 % (3477412)------------------------------
% 64.20/9.39 % (3477412)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 64.20/9.39 % (3477412)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.20/9.39 % (3477412)CaDiCaL version: 2.1.3
% 64.20/9.39 % (3477412)Termination reason: Instruction limit
% 64.20/9.39 % (3477412)Termination phase: Saturation
% 64.20/9.39 % (3477412)Time elapsed: 1.801 s
% 64.20/9.39 % (3477412)Peak memory usage: 28 MB
% 64.20/9.39 % (3477412)Instructions burned: 4592 (million)
% 64.20/9.39 % TRYING [8]
% 64.20/9.39 % (3477416)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=249882673:i=5211_2909 on theBenchmark for (2909ds/5211Mi)
% 64.20/9.39 % (3477352) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3477345-3477352"...
% 64.20/9.39 % (3477352)...printing done.
% 64.20/9.39 % (3477352)Refutation found. Thanks to Tanya!
% 64.20/9.39 % SZS status Unsatisfiable for theBenchmark
% 64.20/9.39 % SZS output start Proof for theBenchmark
% See solution above
% 64.20/9.40 % (3477352)------------------------------
% 64.20/9.40 % (3477352)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 64.20/9.40 % (3477352)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.20/9.40 % (3477352)CaDiCaL version: 2.1.3
% 64.20/9.40 % (3477352)Termination reason: Refutation
% 64.20/9.40 % (3477352)Time elapsed: 9.058 s
% 64.20/9.40 % (3477352)Peak memory usage: 111 MB
% 64.20/9.40 % (3477352)Instructions burned: 20034 (million)
% 64.20/9.40 % (3477345)Success in time 9.156 s
% 64.20/9.40 % Vampire exiting
%------------------------------------------------------------------------------