%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : BOO020-1 : TPTP v9.3.1. Released v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% Computer : n020.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 : Fri Sep 25 01:00:15 PM UTC 2026
% Result : Unsatisfiable 48.83s 8.88s
% Output : CNFRefutation 48.83s
% Verified :
% SZS Type : Refutation
% Derivation depth : 54
% Number of leaves : 4
% Syntax : Number of formulae : 160 ( 107 unt; 0 def)
% Number of atoms : 217 ( 216 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 122 ( 65 ~; 57 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 4 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 6 ( 6 usr; 4 con; 0-2 aty)
% Number of variables : 329 ( 0 sgn 329 !; 0 ?; 320 :)
% 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),inverse(X3)) = n0
| add(add(add(X0,X1),X2),X3) != add(add(X1,X2),X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',frink2) ).
fof(f3,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',frink3) ).
fof(f4,negated_conjecture,
( add(b,a) != add(a,b)
| add(add(a,b),c) != add(a,add(b,c))
| add(inverse(add(a,inverse(b))),inverse(add(inverse(a),inverse(b)))) != b ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_huntington) ).
fof(f5,plain,
( add(a,b) != add(b,a)
| add(add(a,b),c) != add(a,add(b,c))
| b != add(inverse(add(a,inverse(b))),inverse(add(inverse(a),inverse(b)))) ),
inference(reorient_equations,[],[f4]) ).
tcf(c_53,negated_conjecture,
( ( add(a,b) != add(b,a) )
| ( add(add(a,b),c) != add(a,add(b,c)) )
| ( add(inverse(add(a,inverse(b))),inverse(add(inverse(a),inverse(b)))) != b ) ),
inference(cnf_transformation,[],[f5]) ).
tcf(c_54,plain,
! [X0: $i] : add(X0,X0) = X0,
inference(cnf_transformation,[],[f1]) ).
tcf(c_55,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( add(add(add(X0,X1),X2),X3) = add(add(X1,X2),X0) )
| ( add(add(add(X0,X1),X2),inverse(X3)) != n0 ) ),
inference(cnf_transformation,[],[f3]) ).
tcf(c_56,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( add(add(add(X0,X1),X2),inverse(X3)) = n0 )
| ( add(add(add(X0,X1),X2),X3) != add(add(X1,X2),X0) ) ),
inference(cnf_transformation,[],[f2]) ).
tcf(c_180,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( add(add(add(X0,X0),X1),X2) = add(add(X0,X1),X0) )
| ( add(add(X0,X1),inverse(X2)) != n0 ) ),
inference(superposition,[status(thm)],[c_54,c_55]) ).
tcf(c_181,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( add(add(X0,X1),X0) = add(add(X0,X1),X2) )
| ( add(add(X0,X1),inverse(X2)) != n0 ) ),
inference(light_normalisation,[status(thm)],[c_180,c_54]) ).
tcf(c_192,plain,
! [X0: $i,X1: $i] :
( ( add(add(X0,X0),X0) = add(add(X0,X0),X1) )
| ( add(X0,inverse(X1)) != n0 ) ),
inference(superposition,[status(thm)],[c_54,c_181]) ).
tcf(c_193,plain,
! [X0: $i,X1: $i] :
( ( add(X0,X1) = X0 )
| ( add(X0,inverse(X1)) != n0 ) ),
inference(light_normalisation,[status(thm)],[c_192,c_54]) ).
tcf(c_214,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( add(add(add(X0,X0),X1),inverse(X2)) = n0 )
| ( add(add(X0,X1),X0) != add(add(X0,X1),X2) ) ),
inference(superposition,[status(thm)],[c_54,c_56]) ).
tcf(c_215,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( add(add(X0,X1),inverse(X2)) = n0 )
| ( add(add(X0,X1),X0) != add(add(X0,X1),X2) ) ),
inference(light_normalisation,[status(thm)],[c_214,c_54]) ).
tcf(c_231,plain,
! [X0: $i,X1: $i] :
( ( add(add(X0,X0),inverse(X1)) = n0 )
| ( add(X0,X1) != X0 ) ),
inference(superposition,[status(thm)],[c_54,c_215]) ).
tcf(c_232,plain,
! [X0: $i,X1: $i] : add(add(X0,X1),inverse(X0)) = n0,
inference(equality_resolution,[status(thm)],[c_215]) ).
tcf(c_233,plain,
! [X0: $i,X1: $i] :
( ( add(X0,inverse(X1)) = n0 )
| ( add(X0,X1) != X0 ) ),
inference(light_normalisation,[status(thm)],[c_231,c_54]) ).
tcf(c_257,plain,
! [X0: $i] : add(X0,inverse(X0)) = n0,
inference(superposition,[status(thm)],[c_54,c_233]) ).
tcf(c_270,plain,
! [X0: $i,X1: $i,X2: $i] : add(add(add(X0,X1),X2),add(add(X0,X1),X2)) = add(add(X1,X2),X0),
inference(superposition,[status(thm)],[c_257,c_55]) ).
tcf(c_272,plain,
! [X0: $i,X1: $i] : add(add(X0,X1),add(X0,X1)) = add(add(X0,X1),X0),
inference(superposition,[status(thm)],[c_257,c_181]) ).
tcf(c_328,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( add(add(add(X0,X1),add(X0,X1)),X2) = add(add(X1,add(X0,X1)),X0) )
| ( add(add(X0,X1),inverse(X2)) != n0 ) ),
inference(superposition,[status(thm)],[c_54,c_55]) ).
tcf(c_329,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( add(add(add(X0,X0),X1),X2) = add(add(X0,X1),X0) )
| ( add(add(X0,X1),inverse(X2)) != n0 ) ),
inference(superposition,[status(thm)],[c_54,c_55]) ).
tcf(c_330,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( add(add(X0,X1),X0) = add(add(X0,X1),X2) )
| ( add(add(X0,X1),inverse(X2)) != n0 ) ),
inference(light_normalisation,[status(thm)],[c_329,c_54]) ).
tcf(c_351,plain,
! [X0: $i,X1: $i,X2: $i] : add(add(add(X0,X1),X2),add(X0,X1)) = add(add(X1,X2),X0),
inference(demodulation,[status(thm)],[c_270,c_272]) ).
tcf(c_352,plain,
! [X0: $i,X1: $i] : add(add(X0,add(X1,X0)),X1) = add(X1,X0),
inference(superposition,[status(thm)],[c_54,c_351]) ).
tcf(c_419,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( add(add(add(X0,X0),X1),inverse(X2)) = n0 )
| ( add(add(X0,X1),X0) != add(add(X0,X1),X2) ) ),
inference(superposition,[status(thm)],[c_54,c_56]) ).
tcf(c_420,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( add(add(X0,X1),inverse(X2)) = n0 )
| ( add(add(X0,X1),X0) != add(add(X0,X1),X2) ) ),
inference(light_normalisation,[status(thm)],[c_419,c_54]) ).
tcf(c_515,plain,
! [X0: $i,X1: $i] :
( ( add(add(X0,X0),inverse(X1)) = n0 )
| ( add(X0,X1) != X0 ) ),
inference(superposition,[status(thm)],[c_54,c_420]) ).
tcf(c_517,plain,
! [X0: $i,X1: $i] :
( ( add(X0,inverse(X1)) = n0 )
| ( add(X0,X1) != X0 ) ),
inference(light_normalisation,[status(thm)],[c_515,c_54]) ).
tcf(c_526,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( add(add(X1,add(X0,X1)),X0) = add(add(X0,X1),X2) )
| ( add(add(X0,X1),inverse(X2)) != n0 ) ),
inference(demodulation,[status(thm)],[c_328,c_54]) ).
tcf(c_546,plain,
! [X0: $i] : add(X0,inverse(X0)) = n0,
inference(superposition,[status(thm)],[c_54,c_517]) ).
tcf(c_555,plain,
! [X0: $i] : add(n0,inverse(X0)) = n0,
inference(superposition,[status(thm)],[c_257,c_232]) ).
tcf(c_572,plain,
! [X0: $i,X1: $i] : add(add(X0,X1),X0) = add(X0,X1),
inference(superposition,[status(thm)],[c_232,c_193]) ).
tcf(c_574,plain,
! [X0: $i] : add(inverse(X0),X0) = n0,
inference(superposition,[status(thm)],[c_232,c_352]) ).
tcf(c_598,plain,
! [X0: $i,X1: $i,X2: $i] : add(add(X0,X1),X2) = add(add(X1,X2),X0),
inference(demodulation,[status(thm)],[c_351,c_572]) ).
tcf(c_599,plain,
( ( add(a,b) != add(b,a) )
| ( add(add(b,c),a) != add(a,add(b,c)) )
| ( add(inverse(add(a,inverse(b))),inverse(add(inverse(a),inverse(b)))) != b ) ),
inference(demodulation,[status(thm)],[c_53,c_598]) ).
tcf(c_660,plain,
! [X0: $i,X1: $i,X2: $i] : add(add(add(X0,X1),X2),add(add(X0,X1),X2)) = add(add(X1,X2),X0),
inference(superposition,[status(thm)],[c_546,c_55]) ).
tcf(c_661,plain,
! [X0: $i,X1: $i] : add(add(X0,add(X1,X0)),X1) = add(add(X1,X0),add(X1,X0)),
inference(superposition,[status(thm)],[c_546,c_526]) ).
tcf(c_662,plain,
! [X0: $i,X1: $i] : add(add(X0,X1),add(X0,X1)) = add(add(X0,X1),X0),
inference(superposition,[status(thm)],[c_546,c_330]) ).
tcf(c_693,plain,
! [X0: $i] : add(n0,X0) = n0,
inference(superposition,[status(thm)],[c_555,c_193]) ).
tcf(c_710,plain,
! [X0: $i] : add(inverse(inverse(X0)),X0) = inverse(inverse(X0)),
inference(superposition,[status(thm)],[c_574,c_193]) ).
tcf(c_806,plain,
! [X0: $i,X1: $i] : add(add(X0,n0),X1) = add(n0,X0),
inference(superposition,[status(thm)],[c_693,c_598]) ).
tcf(c_839,plain,
! [X0: $i,X1: $i] : add(add(X0,n0),X1) = n0,
inference(light_normalisation,[status(thm)],[c_806,c_693]) ).
tcf(c_1000,plain,
! [X0: $i,X1: $i,X2: $i] : add(add(add(X0,X1),X2),add(X0,X1)) = add(add(X1,X2),X0),
inference(demodulation,[status(thm)],[c_660,c_662]) ).
tcf(c_1018,plain,
! [X0: $i,X1: $i,X2: $i] : add(add(add(X0,X1),X2),inverse(add(X0,X1))) = n0,
inference(superposition,[status(thm)],[c_1000,c_56]) ).
tcf(c_1165,plain,
! [X0: $i] : add(X0,n0) = n0,
inference(superposition,[status(thm)],[c_839,c_572]) ).
tcf(c_1213,plain,
inverse(inverse(n0)) = n0,
inference(superposition,[status(thm)],[c_1165,c_710]) ).
tcf(c_1260,plain,
! [X0: $i] :
( ( add(X0,inverse(n0)) = X0 )
| ( add(X0,n0) != n0 ) ),
inference(superposition,[status(thm)],[c_1213,c_193]) ).
tcf(c_1262,plain,
! [X0: $i] : add(X0,inverse(n0)) = X0,
inference(ground_joinability,[status(thm)],[c_1260,c_1165]) ).
tcf(c_1278,plain,
! [X0: $i,X1: $i] : add(add(X0,inverse(n0)),X1) = add(X1,X0),
inference(superposition,[status(thm)],[c_1262,c_598]) ).
tcf(c_1290,plain,
! [X0: $i,X1: $i] : add(X0,X1) = add(X1,X0),
inference(light_normalisation,[status(thm)],[c_1278,c_1262]) ).
tcf(c_1308,plain,
add(inverse(add(a,inverse(b))),inverse(add(inverse(a),inverse(b)))) != b,
inference(backward_subsumption_resolution,[status(thm)],[c_599,c_1290]) ).
tcf(c_2175,plain,
! [X0: $i,X1: $i] : add(add(X0,X1),inverse(X0)) = n0,
inference(superposition,[status(thm)],[c_54,c_1018]) ).
tcf(c_2179,plain,
! [X0: $i] : add(X0,inverse(X0)) = n0,
inference(superposition,[status(thm)],[c_54,c_2175]) ).
tcf(c_2185,plain,
! [X0: $i,X1: $i] : add(add(X0,X1),X0) = add(X0,X1),
inference(demodulation,[status(thm)],[c_662,c_54]) ).
tcf(c_2188,plain,
! [X0: $i] : add(n0,X0) = n0,
inference(superposition,[status(thm)],[c_2179,c_2185]) ).
tcf(c_2192,plain,
! [X0: $i,X1: $i] : add(add(X0,add(X1,X0)),X1) = add(X1,X0),
inference(demodulation,[status(thm)],[c_661,c_54]) ).
tcf(c_2210,plain,
! [X0: $i,X1: $i,X2: $i] : add(add(add(X0,X1),X2),add(X0,X1)) = add(add(X1,X2),X0),
inference(superposition,[status(thm)],[c_2175,c_55]) ).
tcf(c_2211,plain,
! [X0: $i,X1: $i,X2: $i] : add(add(add(X0,X1),X2),add(add(X0,X1),X2)) = add(add(X1,X2),X0),
inference(superposition,[status(thm)],[c_2179,c_55]) ).
tcf(c_2212,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( add(add(add(X0,X1),add(X0,X1)),X2) = add(add(X1,add(X0,X1)),X0) )
| ( add(add(X0,X1),inverse(X2)) != n0 ) ),
inference(superposition,[status(thm)],[c_54,c_55]) ).
tcf(c_2219,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( add(add(add(add(X1,add(X0,X1)),X0),X2),X3) = add(add(X0,X2),add(X1,add(X0,X1))) )
| ( add(add(add(X0,X1),X2),inverse(X3)) != n0 ) ),
inference(superposition,[status(thm)],[c_2192,c_55]) ).
tcf(c_2258,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( add(add(add(X2,X0),X1),inverse(inverse(add(X2,X0)))) = n0 )
| ( add(add(X0,X1),X2) != n0 ) ),
inference(superposition,[status(thm)],[c_2175,c_56]) ).
tcf(c_2304,plain,
! [X0: $i,X1: $i,X2: $i] : add(add(X0,X1),X2) = add(add(X1,X2),X0),
inference(demodulation,[status(thm)],[c_2210,c_2185]) ).
tcf(c_2311,plain,
! [X0: $i,X1: $i,X2: $i] : add(add(X0,X1),add(X0,X2)) = add(add(X0,X2),X1),
inference(superposition,[status(thm)],[c_2185,c_2304]) ).
tcf(c_2320,plain,
! [X0: $i,X1: $i,X2: $i] : add(add(X0,add(X1,X2)),X1) = add(add(X1,X2),X0),
inference(superposition,[status(thm)],[c_2185,c_2304]) ).
tcf(c_2322,plain,
! [X0: $i,X1: $i] : add(add(X0,X1),inverse(X1)) = add(n0,X0),
inference(superposition,[status(thm)],[c_2179,c_2304]) ).
tcf(c_2323,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : add(add(add(X0,X1),X2),X3) = add(add(X1,X3),add(X2,X0)),
inference(superposition,[status(thm)],[c_2304,c_2304]) ).
tcf(c_2334,plain,
! [X0: $i,X1: $i] : add(add(X0,X1),X1) = add(X1,X0),
inference(superposition,[status(thm)],[c_2304,c_2185]) ).
tcf(c_2350,plain,
! [X0: $i,X1: $i] : add(add(X0,X1),inverse(X1)) = n0,
inference(light_normalisation,[status(thm)],[c_2322,c_2188]) ).
tcf(c_2837,plain,
! [X0: $i,X1: $i,X2: $i] : add(add(X0,X1),add(X1,X2)) = add(add(X0,X1),X2),
inference(demodulation,[status(thm)],[c_2211,c_2323,c_2311]) ).
tcf(c_2841,plain,
! [X0: $i,X1: $i] : add(X0,add(X0,X1)) = add(X0,X1),
inference(superposition,[status(thm)],[c_54,c_2837]) ).
tcf(c_2867,plain,
! [X0: $i,X1: $i] : add(add(add(X0,X1),X0),X1) = add(add(X0,X1),X0),
inference(superposition,[status(thm)],[c_2837,c_2185]) ).
tcf(c_2870,plain,
! [X0: $i,X1: $i] : add(X0,X1) = add(X1,X0),
inference(light_normalisation,[status(thm)],[c_2867,c_2185,c_2334]) ).
tcf(c_4082,plain,
! [X0: $i,X1: $i,X2: $i] : add(add(X0,X1),X2) = add(X1,add(X2,X0)),
inference(superposition,[status(thm)],[c_2870,c_2304]) ).
tcf(c_4088,plain,
! [X0: $i,X1: $i,X2: $i] : add(add(X0,X1),X2) = add(X0,add(X1,X2)),
inference(superposition,[status(thm)],[c_2870,c_2304]) ).
tcf(c_4090,plain,
! [X0: $i] : add(X0,n0) = n0,
inference(superposition,[status(thm)],[c_2870,c_2188]) ).
tcf(c_4806,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( add(add(add(X1,X2),X0),inverse(inverse(add(X1,X2)))) = n0 )
| ( add(X0,add(X1,X2)) != n0 ) ),
inference(light_normalisation,[status(thm)],[c_2258,c_4082]) ).
tcf(c_4807,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( add(X0,add(X2,add(X1,inverse(inverse(add(X1,X2)))))) = n0 )
| ( add(X0,add(X1,X2)) != n0 ) ),
inference(demodulation,[status(thm)],[c_4806,c_2870,c_4082]) ).
tcf(c_4819,plain,
! [X0: $i,X1: $i] :
( ( add(X0,add(X1,add(X1,inverse(inverse(add(X1,X1)))))) = n0 )
| ( add(X0,X1) != n0 ) ),
inference(superposition,[status(thm)],[c_54,c_4807]) ).
tcf(c_5223,plain,
! [X0: $i,X1: $i] :
( ( add(X0,add(X1,inverse(inverse(X1)))) = n0 )
| ( add(X0,X1) != n0 ) ),
inference(demodulation,[status(thm)],[c_4819,c_54,c_2841]) ).
tcf(c_5236,plain,
! [X0: $i] : add(X0,add(n0,inverse(inverse(n0)))) = n0,
inference(superposition,[status(thm)],[c_4090,c_5223]) ).
tcf(c_5289,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( add(X0,add(X1,X2)) = add(X0,X2) )
| ( add(X0,add(inverse(X1),X2)) != n0 ) ),
inference(demodulation,[status(thm)],[c_2212,c_2334,c_2320,c_2841,c_4082]) ).
tcf(c_5304,plain,
! [X0: $i,X1: $i] :
( ( add(X0,add(X1,inverse(inverse(X1)))) = add(X0,inverse(inverse(X1))) )
| ( add(X0,n0) != n0 ) ),
inference(superposition,[status(thm)],[c_2179,c_5289]) ).
tcf(c_5316,plain,
! [X0: $i,X1: $i] : add(X0,add(X1,inverse(inverse(X1)))) = add(X0,inverse(inverse(X1))),
inference(ground_joinability,[status(thm)],[c_5304,c_4090]) ).
tcf(c_7075,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( add(add(add(add(X0,add(X2,X0)),X2),X1),X3) = add(add(X2,X1),add(X0,add(X2,X0))) )
| ( add(add(X0,add(X1,X2)),inverse(X3)) != n0 ) ),
inference(light_normalisation,[status(thm)],[c_2219,c_4082]) ).
tcf(c_7076,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( add(X2,add(X3,add(X1,X0))) = add(X2,add(X1,X0)) )
| ( add(X0,add(X1,add(X2,inverse(X3)))) != n0 ) ),
inference(demodulation,[status(thm)],[c_7075,c_2334,c_2320,c_4082]) ).
tcf(c_7706,plain,
! [X0: $i,X1: $i] : add(X0,add(inverse(X0),X1)) = n0,
inference(demodulation,[status(thm)],[c_2350,c_4082]) ).
tcf(c_7727,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( add(inverse(X1),add(X2,add(X1,X0))) = add(inverse(X1),add(X1,X0)) )
| ( add(X0,n0) != n0 ) ),
inference(superposition,[status(thm)],[c_7706,c_7076]) ).
tcf(c_7732,plain,
! [X0: $i,X1: $i,X2: $i] : add(inverse(X0),add(X1,add(X0,X2))) = add(inverse(X0),add(X0,X2)),
inference(ground_joinability,[status(thm)],[c_7727,c_4090]) ).
tcf(c_11240,plain,
! [X0: $i] : add(X0,inverse(inverse(n0))) = n0,
inference(demodulation,[status(thm)],[c_5236,c_5316]) ).
tcf(c_11244,plain,
inverse(inverse(n0)) = n0,
inference(superposition,[status(thm)],[c_11240,c_54]) ).
tcf(c_11343,plain,
! [X0: $i,X1: $i] :
( ( add(X0,add(inverse(n0),X1)) = add(X0,X1) )
| ( add(X0,add(n0,X1)) != n0 ) ),
inference(superposition,[status(thm)],[c_11244,c_5289]) ).
tcf(c_11346,plain,
! [X0: $i,X1: $i] : add(X0,add(inverse(n0),X1)) = add(X0,X1),
inference(ground_joinability,[status(thm)],[c_11343,c_2188,c_4090]) ).
tcf(c_14987,plain,
! [X0: $i,X1: $i] : add(X0,add(X1,inverse(n0))) = add(X0,X1),
inference(superposition,[status(thm)],[c_2870,c_11346]) ).
tcf(c_27927,plain,
! [X0: $i,X1: $i,X2: $i] : add(X0,add(X1,X2)) = add(X1,add(X0,X2)),
inference(superposition,[status(thm)],[c_4088,c_2870]) ).
tcf(c_27928,negated_conjecture,
add(inverse(add(a,inverse(b))),inverse(add(inverse(a),inverse(b)))) != b,
inference(global_subsumption_just,[status(thm)],[c_53,c_1308]) ).
tcf(c_27930,plain,
add(inverse(add(a,inverse(b))),inverse(add(inverse(b),inverse(a)))) != b,
inference(theory_normalisation,[status(thm)],[c_27928,c_4088,c_2870]) ).
tcf(c_27931,plain,
! [X0: $i] : add(n0,X0) = n0,
inference(superposition,[status(thm)],[c_4090,c_2870]) ).
tcf(c_27943,plain,
! [X0: $i,X1: $i] : add(X0,add(inverse(n0),X1)) = add(X0,X1),
inference(superposition,[status(thm)],[c_2870,c_14987]) ).
tcf(c_27962,plain,
! [X0: $i,X1: $i] : add(add(inverse(n0),X0),X1) = add(X1,X0),
inference(superposition,[status(thm)],[c_27943,c_2870]) ).
tcf(c_27965,plain,
! [X0: $i,X1: $i] : add(inverse(n0),add(X0,X1)) = add(X1,X0),
inference(theory_normalisation,[status(thm)],[c_27962,c_4088,c_2870]) ).
tcf(c_27971,plain,
! [X0: $i,X1: $i,X2: $i] : add(X0,add(X1,add(X2,X1))) = add(X1,add(X2,X0)),
inference(theory_normalisation,[status(thm)],[c_2320,c_4088,c_2870]) ).
tcf(c_27981,plain,
! [X0: $i,X1: $i] : add(X0,add(X0,X1)) = add(X1,X0),
inference(superposition,[status(thm)],[c_54,c_27971]) ).
tcf(c_27982,plain,
! [X0: $i,X1: $i,X2: $i] : add(X0,add(X1,add(X1,X2))) = add(X1,add(X2,X0)),
inference(superposition,[status(thm)],[c_2870,c_27971]) ).
tcf(c_28012,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( add(X0,add(X1,add(X2,X3))) = add(X1,add(X2,X0)) )
| ( add(X0,add(X1,add(X2,inverse(X3)))) != n0 ) ),
inference(theory_normalisation,[status(thm)],[c_55,c_4088,c_2870]) ).
tcf(c_28144,plain,
! [X0: $i,X1: $i] : add(add(inverse(n0),X0),X1) = add(X1,add(X1,X0)),
inference(superposition,[status(thm)],[c_27943,c_27981]) ).
tcf(c_28154,plain,
! [X0: $i] : add(inverse(n0),X0) = add(X0,X0),
inference(superposition,[status(thm)],[c_27981,c_14987]) ).
tcf(c_28156,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( add(X0,add(X2,add(X2,X1))) = add(X2,add(X2,X0)) )
| ( add(X0,add(inverse(X1),X2)) != n0 ) ),
inference(superposition,[status(thm)],[c_27981,c_28012]) ).
tcf(c_28161,plain,
! [X0: $i] : add(inverse(n0),X0) = X0,
inference(light_normalisation,[status(thm)],[c_28154,c_54]) ).
tcf(c_28164,plain,
! [X0: $i,X1: $i] : add(inverse(n0),add(X0,X1)) = add(X1,add(X1,X0)),
inference(theory_normalisation,[status(thm)],[c_28144,c_4088,c_2870]) ).
tcf(c_28165,plain,
! [X0: $i,X1: $i] : add(X0,add(X0,X1)) = add(X0,X1),
inference(light_normalisation,[status(thm)],[c_28164,c_27965]) ).
tcf(c_28184,plain,
! [X0: $i,X1: $i,X2: $i] : add(X0,add(X1,add(X2,inverse(add(X0,X1))))) = n0,
inference(theory_normalisation,[status(thm)],[c_1018,c_4088,c_2870]) ).
tcf(c_28188,plain,
! [X0: $i,X1: $i] : add(X0,add(X1,inverse(add(X0,X1)))) = n0,
inference(superposition,[status(thm)],[c_54,c_28184]) ).
tcf(c_28278,plain,
! [X0: $i,X1: $i,X2: $i] : add(X0,add(X1,add(X2,inverse(X0)))) = add(X0,add(X2,inverse(X0))),
inference(theory_normalisation,[status(thm)],[c_7732,c_4088,c_2870]) ).
tcf(c_28285,plain,
! [X0: $i,X1: $i] : add(X0,add(X1,inverse(X0))) = add(X0,n0),
inference(superposition,[status(thm)],[c_27931,c_28278]) ).
tcf(c_28288,plain,
! [X0: $i,X1: $i] : add(X0,add(X1,inverse(X0))) = add(X0,inverse(X0)),
inference(superposition,[status(thm)],[c_54,c_28278]) ).
tcf(c_28304,plain,
! [X0: $i,X1: $i] : add(X0,add(X1,inverse(X0))) = n0,
inference(light_normalisation,[status(thm)],[c_28285,c_4090]) ).
tcf(c_28339,plain,
! [X0: $i] : add(X0,inverse(n0)) = X0,
inference(superposition,[status(thm)],[c_28161,c_27981]) ).
tcf(c_28352,plain,
! [X0: $i,X1: $i] : add(X0,add(X1,inverse(add(inverse(n0),X0)))) = n0,
inference(superposition,[status(thm)],[c_28161,c_28184]) ).
tcf(c_28353,plain,
! [X0: $i] : add(X0,inverse(X0)) = n0,
inference(light_normalisation,[status(thm)],[c_28352,c_28161,c_28288]) ).
tcf(c_28402,plain,
! [X0: $i,X1: $i] : add(X0,add(inverse(X0),X1)) = n0,
inference(superposition,[status(thm)],[c_2870,c_28304]) ).
tcf(c_28969,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( add(X2,add(X1,X0)) = add(X2,X0) )
| ( add(X0,add(inverse(X1),X2)) != n0 ) ),
inference(demodulation,[status(thm)],[c_28156,c_28165,c_27982]) ).
tcf(c_28993,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( add(X1,add(X2,X0)) = add(X1,X0) )
| ( add(X0,add(X1,inverse(X2))) != n0 ) ),
inference(superposition,[status(thm)],[c_2870,c_28969]) ).
tcf(c_30129,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( add(X0,add(X1,X2)) = add(X0,X2) )
| ( add(add(X0,inverse(X1)),X2) != n0 ) ),
inference(superposition,[status(thm)],[c_2870,c_28993]) ).
tcf(c_30133,plain,
! [X0: $i,X1: $i] :
( ( add(X1,add(X0,X1)) = add(X1,X1) )
| ( add(inverse(X0),X1) != n0 ) ),
inference(superposition,[status(thm)],[c_27981,c_28993]) ).
tcf(c_30168,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( add(X0,add(X1,X2)) = add(X0,X2) )
| ( add(X0,add(inverse(X1),X2)) != n0 ) ),
inference(theory_normalisation,[status(thm)],[c_30129,c_4088,c_2870]) ).
tcf(c_30191,plain,
! [X0: $i,X1: $i] :
( ( add(X1,add(X0,X1)) = X1 )
| ( add(inverse(X0),X1) != n0 ) ),
inference(demodulation,[status(thm)],[c_30133,c_54]) ).
tcf(c_30201,plain,
! [X0: $i] : add(inverse(inverse(X0)),add(X0,inverse(inverse(X0)))) = inverse(inverse(X0)),
inference(superposition,[status(thm)],[c_28353,c_30191]) ).
tcf(c_30222,plain,
! [X0: $i] : add(X0,add(inverse(inverse(X0)),inverse(inverse(X0)))) = inverse(inverse(X0)),
inference(theory_normalisation,[status(thm)],[c_30201,c_4088,c_2870]) ).
tcf(c_31201,plain,
! [X0: $i,X1: $i] :
( ( add(inverse(n0),add(X0,X1)) = add(inverse(n0),X1) )
| ( add(inverse(X0),X1) != n0 ) ),
inference(superposition,[status(thm)],[c_28161,c_30168]) ).
tcf(c_31218,plain,
! [X0: $i,X1: $i] :
( ( add(X0,add(X1,inverse(inverse(X1)))) = add(X0,inverse(inverse(X1))) )
| ( add(X0,n0) != n0 ) ),
inference(superposition,[status(thm)],[c_28353,c_30168]) ).
tcf(c_31249,plain,
! [X0: $i,X1: $i] : add(X0,add(X1,inverse(inverse(X1)))) = add(X0,inverse(inverse(X1))),
inference(ground_joinability,[status(thm)],[c_31218,c_4090]) ).
tcf(c_31311,plain,
! [X0: $i] : add(add(X0,inverse(inverse(X0))),inverse(inverse(X0))) = add(X0,inverse(inverse(X0))),
inference(superposition,[status(thm)],[c_31249,c_54]) ).
tcf(c_31346,plain,
! [X0: $i] : add(X0,inverse(inverse(inverse(X0)))) = n0,
inference(superposition,[status(thm)],[c_31249,c_28402]) ).
tcf(c_31370,plain,
! [X0: $i] : add(X0,add(inverse(inverse(X0)),inverse(inverse(X0)))) = add(X0,inverse(inverse(X0))),
inference(theory_normalisation,[status(thm)],[c_31311,c_4088,c_2870]) ).
tcf(c_31371,plain,
! [X0: $i] : add(X0,inverse(inverse(X0))) = inverse(inverse(X0)),
inference(light_normalisation,[status(thm)],[c_31370,c_30222]) ).
tcf(c_31489,plain,
! [X0: $i,X1: $i] :
( ( add(X1,add(inverse(inverse(X1)),X0)) = add(X1,X0) )
| ( add(X0,n0) != n0 ) ),
inference(superposition,[status(thm)],[c_31346,c_28993]) ).
tcf(c_31519,plain,
! [X0: $i,X1: $i] : add(X0,add(inverse(inverse(X0)),X1)) = add(X0,X1),
inference(ground_joinability,[status(thm)],[c_31489,c_4090]) ).
tcf(c_31785,plain,
! [X0: $i,X1: $i] : add(X0,add(inverse(inverse(X0)),X1)) = add(inverse(inverse(X0)),X1),
inference(superposition,[status(thm)],[c_31371,c_4088]) ).
tcf(c_31817,plain,
! [X0: $i,X1: $i] : add(inverse(inverse(X0)),X1) = add(X0,X1),
inference(light_normalisation,[status(thm)],[c_31785,c_31519]) ).
tcf(c_32495,plain,
! [X0: $i] : add(X0,inverse(n0)) = inverse(inverse(X0)),
inference(superposition,[status(thm)],[c_31817,c_28339]) ).
tcf(c_32533,plain,
! [X0: $i] : inverse(inverse(X0)) = X0,
inference(light_normalisation,[status(thm)],[c_32495,c_28339]) ).
tcf(c_37085,plain,
! [X0: $i,X1: $i] :
( ( add(X0,X1) = X1 )
| ( add(inverse(X0),X1) != n0 ) ),
inference(demodulation,[status(thm)],[c_31201,c_28161]) ).
tcf(c_37093,plain,
! [X0: $i,X1: $i] :
( ( add(X1,X0) = X0 )
| ( add(X0,inverse(X1)) != n0 ) ),
inference(superposition,[status(thm)],[c_2870,c_37085]) ).
tcf(c_37115,plain,
! [X0: $i,X1: $i] :
( ( add(inverse(X0),X1) = X1 )
| ( add(X0,X1) != n0 ) ),
inference(superposition,[status(thm)],[c_32533,c_37085]) ).
tcf(c_43280,plain,
! [X0: $i,X1: $i] :
( ( add(inverse(X1),X0) = X0 )
| ( add(X0,X1) != n0 ) ),
inference(superposition,[status(thm)],[c_32533,c_37093]) ).
tcf(c_43319,plain,
! [X0: $i,X1: $i] : add(inverse(X0),add(X1,inverse(add(X0,X1)))) = add(X1,inverse(add(X0,X1))),
inference(superposition,[status(thm)],[c_28188,c_37115]) ).
tcf(c_44872,plain,
! [X0: $i,X1: $i] : add(inverse(add(inverse(X0),X1)),X0) = X0,
inference(superposition,[status(thm)],[c_28402,c_43280]) ).
tcf(c_44873,plain,
! [X0: $i,X1: $i] : add(inverse(add(X0,inverse(X1))),X1) = X1,
inference(superposition,[status(thm)],[c_28304,c_43280]) ).
tcf(c_44891,plain,
! [X0: $i,X1: $i] : add(X0,inverse(add(X1,inverse(X0)))) = X0,
inference(theory_normalisation,[status(thm)],[c_44873,c_4088,c_2870]) ).
tcf(c_44892,plain,
! [X0: $i,X1: $i] : add(X0,inverse(add(inverse(X0),X1))) = X0,
inference(theory_normalisation,[status(thm)],[c_44872,c_4088,c_2870]) ).
tcf(c_46387,plain,
! [X0: $i,X1: $i] : add(inverse(X0),inverse(add(X1,X0))) = inverse(X0),
inference(superposition,[status(thm)],[c_32533,c_44891]) ).
tcf(c_47004,plain,
! [X0: $i,X1: $i] : add(inverse(X0),inverse(add(X0,X1))) = inverse(X0),
inference(superposition,[status(thm)],[c_32533,c_44892]) ).
tcf(c_51301,plain,
! [X0: $i,X1: $i,X2: $i] : add(inverse(X0),add(X1,inverse(add(X0,X2)))) = add(X1,inverse(X0)),
inference(superposition,[status(thm)],[c_47004,c_27927]) ).
tcf(c_51407,plain,
! [X0: $i,X1: $i] : add(X0,inverse(add(X1,X0))) = add(X0,inverse(X1)),
inference(demodulation,[status(thm)],[c_43319,c_51301]) ).
tcf(c_56336,plain,
! [X0: $i,X1: $i] : add(inverse(add(X0,X1)),inverse(add(X1,inverse(X0)))) = add(inverse(add(X0,X1)),inverse(X1)),
inference(superposition,[status(thm)],[c_51407,c_51407]) ).
tcf(c_56399,plain,
! [X0: $i,X1: $i] : add(inverse(add(X0,X1)),inverse(add(X1,inverse(X0)))) = add(inverse(X1),inverse(add(X0,X1))),
inference(theory_normalisation,[status(thm)],[c_56336,c_4088,c_2870]) ).
tcf(c_56454,plain,
add(inverse(inverse(b)),inverse(add(a,inverse(b)))) != b,
inference(demodulation,[status(thm)],[c_27930,c_56399]) ).
tcf(c_56455,plain,
$false,
inference(ground_joinability,[status(thm)],[c_56454,c_32533,c_46387]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : BOO020-1 : TPTP v9.3.1. Released v2.2.0.
% 0.00/0.03 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.10/0.37 % Computer : n020.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Fri Sep 25 06:35:20 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.10/0.41 Running first-order theorem proving
% 0.10/0.41 Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.42
% 0.10/0.42 % ======== iProver multi-core TPTP/SMT =========
% 0.10/0.42
% 0.10/0.42 % Detected problem language: tptp
% 0.10/0.44 % Proving...
% 48.83/8.88 % SZS status Started for theBenchmark.p
% 48.83/8.88 ERROR - "ProverProcess:heur/330959:296.0" ran with exit code 2 and error: iprover.ml: Unexpected exception: Failure("Clause.get_demod_eqs: not a demod/lightnorm conclusion ( add(n0,inverse(X0)) = n0 )")
% 48.83/8.88 Fatal error: exception Failure("Clause.get_demod_eqs: not a demod/lightnorm conclusion ( add(n0,inverse(X0)) = n0 )")
% 48.83/8.88 ERROR - cmd was: ulimit -v 4023281; ./res/iproveropt --abstr_ref "[]" --abstr_ref_af_restrict_to_split_sk false --abstr_ref_prep false --abstr_ref_sig_restrict funpre --abstr_ref_under "[]" --abstr_ref_until_sat false --add_important_lit false --bc_imp_inh "[conj_cone]" --brand_transform false --clause_weak_htbl true --comb_inst_mult 3 --comb_mode clause_based --comb_res_mult 1 --comb_sup_deep_mult 2 --comb_sup_mult 0 --conj_cone_tolerance 3. --demod_completeness_check fast --demod_use_ground true --eq_ax_congr_red true --extra_neg_conj none --gc_record_bc_elim false --inst_activity_threshold 500 --inst_dismatching true --inst_eager_unprocessed_to_passive true --inst_eq_res_simp false --inst_learning_factor 2 --inst_learning_loop_flag true --inst_learning_start 3000 --inst_lit_activity_flag true --inst_lit_sel "[+prop;+sign;+ground;-num_var;-num_symb]" --inst_lit_sel_side num_symb --inst_orphan_elimination true --inst_passive_queue_type priority_queues --inst_passive_queues "[[-conj_dist;+conj_symb;-num_var];[+age;-num_symb]]" --inst_passive_queues_freq "[25;2]" --inst_prop_sim_given true --inst_prop_sim_new false --inst_restr_to_given false --inst_sel_renew solver --inst_solver_calls_frac 1. --inst_solver_per_active 1400 --inst_sos_flag false --inst_sos_phase true --inst_sos_sth_lit_sel "[+prop;+non_prol_conj_symb;-eq;+ground;-num_var]" --inst_start_prop_sim_after_learn 3 --inst_subs_given false --inst_subs_new false --instantiation_flag true --large_theory_mode true --lt_threshold 2000 --min_unsat_core false --non_eq_to_eq false --pred_elim true --prep_def_merge true --prep_def_merge_mbd true --prep_def_merge_prop_impl false --prep_def_merge_tr_cl false --prep_def_merge_tr_red false --prep_gs_sim true --prep_res_sim true --prep_sem_filter exhaustive --prep_sem_filter_out false --prep_sup_sim_all true --prep_sup_sim_sup false --prep_unflatten true --prep_upred true --preprocessed_out false --preprocessed_stats false --preprocessing_flag true --prolific_symb_bound 256 --prop_impl_unit "[]" --prop_impl_unit_size 0 --prop_solver_per_cl 1024 --pure_diseq_elim true --res_backward_subs full --res_backward_subs_resolution true --res_forward_subs full --res_forward_subs_resolution true --res_lit_sel adaptive --res_lit_sel_side none --res_ordering kbo --res_orphan_elimination true --res_passive_queue_type priority_queues --res_passive_queues "[[-conj_dist;+conj_symb;-num_symb];[+age;-num_symb]]" --res_passive_queues_freq "[15;5]" --res_prop_simpl_given true --res_prop_simpl_new false --res_sim_input true --res_time_limit 300. --res_to_prop_solver active --reset_solvers false --resolution_flag true --schedule none --share_sel_clauses true --smt_ac_axioms fast --smt_preprocessing true --soft_assumptions false --soft_lemma_size 3 --splitting_cvd false --splitting_cvd_svl false --splitting_grd true --splitting_mode input --splitting_nvd 32 --stats_out none --sub_typing true --subs_bck_mult 8 --sup_full_bw "[BwDemod;BwUnitSubsAndRes]" --sup_full_fw "[FwDemodLightNormLoopTriv;FwUnitSubsAndRes;FwSubsumption;FwSubsumptionRes]" --sup_full_triv "[PropSubs]" --sup_fun_splitting false --sup_immed_bw_immed "[BwUnitSubsAndRes]" --sup_immed_bw_main "[BwUnitSubsAndRes]" --sup_immed_fw_immed "[ACNormalisation;FwDemodLightNormLoopTriv;FwUnitSubsAndRes]" --sup_immed_fw_main "[FwUnitSubsAndRes]" --sup_immed_triv "[]" --sup_indices_passive "[LightNormIndex;UnitSubsumptionIndex]" --sup_input_bw "[BwDemod;BwUnitSubsAndRes;BwSubsumption;BwSubsumptionRes]" --sup_input_fw "[ACNormalisation;FwDemodLightNormLoopTriv;FwUnitSubsAndRes;FwSubsumption;FwSubsumptionRes]" --sup_input_triv "[Unflattening]" --sup_iter_deepening 2 --sup_passive_queue_type priority_queues --sup_passive_queues "[[-conj_dist;-num_symb];[+age;-num_symb];[+score;-num_symb]]" --sup_passive_queues_freq "[8;4;4]" --sup_prop_simpl_given true --sup_prop_simpl_new true --sup_restarts_mult 2 --sup_score sim_d_gen --sup_share_max_num_cl 500 --sup_share_score_frac 0.2 --sup_smt_interval 10000 --sup_symb_ordering invfreq --sup_to_prop_solver passive --superposition_flag true --time_out_prep_mult 0.1 --suppress_sat_res true --tptp_safe_out true --out_options none --proof_out true --sat_out_model pos --clausifier res/vclausify_rel --clausifier_options "--mode clausify -t 98.67" --time_out_real 296.00 /export/starexec/sandbox/benchmark/theBenchmark.p 1>> /export/starexec/sandbox/tmp/iprover_out_o3o2pyi_/669fpywq 2>> /export/starexec/sandbox/tmp/iprover_out_o3o2pyi_/669fpywq_error
% 48.83/8.88 ERROR - "ProverProcess:heur/445550:16.0" ran with exit code 2 and error: iprover.ml: Unexpected exception: Failure("Clause.get_demod_eqs: not a demod/lightnorm conclusion ( add(add(add(X0,X1),X2),X2) = add(add(X1,X2),X0) )")
% 48.83/8.88 Fatal error: exception Failure("Clause.get_demod_eqs: not a demod/lightnorm conclusion ( add(add(add(X0,X1),X2),X2) = add(add(X1,X2),X0) )")
% 48.83/8.88 ERROR - cmd was: ulimit -v 4023281; ./res/iproveropt --abstr_ref "[]" --abstr_ref_under "[]" --comb_inst_mult 3 --comb_mode time_based --comb_res_mult 1 --comb_sup_deep_mult 2 --comb_sup_mult 0 --conj_cone_tolerance 1.6084091637003026 --demod_completeness_check fast --demod_use_ground true --eq_ax_congr_red true --extra_neg_conj none --inst_activity_threshold 500 --inst_dismatching true --inst_eager_unprocessed_to_passive true --inst_eq_res_simp false --inst_learning_factor 2 --inst_learning_loop_flag true --inst_learning_start 3000 --inst_lit_activity_flag true --inst_lit_sel "[+prop;+sign;+ground;-num_var;-num_symb]" --inst_lit_sel_side num_symb --inst_orphan_elimination true --inst_passive_queue_type priority_queues --inst_passive_queues "[[-conj_dist;+conj_symb;-num_var];[+age;-num_symb]]" --inst_passive_queues_freq "[25;2]" --inst_prop_sim_given true --inst_prop_sim_new false --inst_restr_to_given false --inst_sel_renew solver --inst_solver_calls_frac 1. --inst_solver_per_active 1400 --inst_sos_flag false --inst_start_prop_sim_after_learn 3 --inst_subs_given false --inst_subs_new false --instantiation_flag true --out_options none --pred_elim true --prep_def_merge true --prep_def_merge_mbd false --prep_def_merge_prop_impl false --prep_def_merge_tr_cl false --prep_def_merge_tr_red true --prep_gs_sim false --prep_res_sim true --prep_sem_filter neg --prep_sup_sim_all true --prep_sup_sim_sup true --prep_unflatten true --prep_upred false --preprocessing_flag true --prolific_symb_bound 32768 --prop_solver_per_cl 4096 --pure_diseq_elim false --res_backward_subs subset_subsumption --res_backward_subs_resolution false --res_forward_subs subset_subsumption --res_forward_subs_resolution false --res_lit_sel adaptive --res_lit_sel_side num_var --res_ordering kbo --res_passive_queue_type stack --res_passive_queues "[[-num_lits;+conj_symb;-num_symb];[-num_lits;+min_def_symb]]" --res_passive_queues_freq "[1;3]" --res_prop_simpl_given true --res_prop_simpl_new false --res_sim_input false --res_time_limit 202.19 --res_to_prop_solver active --resolution_flag true --schedule none --share_sel_clauses true --smt_ac_axioms fast --smt_preprocessing true --splitting_cvd false --splitting_cvd_svl true --splitting_grd true --splitting_mode input --splitting_nvd 16 --stats_out none --sub_typing false --subs_bck_mult 1 --sup_full_bw "[]" --sup_full_fw "[]" --sup_full_triv "[PropSubs]" --sup_fun_splitting false --sup_immed_bw_immed "[]" --sup_immed_bw_main "[]" --sup_immed_fw_immed "[ACNormalisation]" --sup_immed_fw_main "[]" --sup_immed_triv "[]" --sup_indices_passive "[]" --sup_input_bw "[]" --sup_input_fw "[DemodLightNormLoopTriv;ACNormalisation]" --sup_input_triv "[Unflattening]" --sup_iter_deepening 2 --sup_passive_queue_type priority_queues --sup_passive_queues "[[-conj_dist;-num_symb];[+age;-num_symb];[+score;-num_symb]]" --sup_passive_queues_freq "[8;4;4]" --sup_prop_simpl_given true --sup_prop_simpl_new true --sup_restarts_mult 2 --sup_score sim_d_gen --sup_share_max_num_cl 640 --sup_share_score_frac 0.1 --sup_smt_interval 10000 --sup_symb_ordering invfreq --sup_to_prop_solver passive --superposition_flag true --time_out_prep_mult 0.9903106699302947 --suppress_sat_res true --tptp_safe_out true --proof_out true --sat_out_model pos --clausifier res/vclausify_rel --clausifier_options "--mode clausify -t 5.33" --time_out_real 16.00 /export/starexec/sandbox/benchmark/theBenchmark.p 1>> /export/starexec/sandbox/tmp/iprover_out_o3o2pyi_/6iuocqje 2>> /export/starexec/sandbox/tmp/iprover_out_o3o2pyi_/6iuocqje_error
% 48.83/8.88 % SZS status Unsatisfiable for theBenchmark.p
% 48.83/8.88
% 48.83/8.88 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 48.83/8.88
% 48.83/8.88 % ------ iProver source info
% 48.83/8.88
% 48.83/8.88 % git: date: 2026-07-19 20:42:38 +0200
% 48.83/8.88 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 48.83/8.88 % git: non_committed_changes: false
% 48.83/8.88
% 48.83/8.88 % ------ Parsing...% successful
% 48.83/8.88
% 48.83/8.88
% 48.83/8.88 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 48.83/8.88
% 48.83/8.88 % ------ Preprocessing... sup_sim: 0 sf_s rm: 0 0s sf_e pe_s pe_e %
% 48.83/8.88
% 48.83/8.88 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 48.83/8.88
% 48.83/8.88 % ------ Preprocessing... sf_s rm: 0 0s sf_e
% 48.83/8.88 % ------ Proving...
% 48.83/8.88 % ------ Problem Properties
% 48.83/8.88
% 48.83/8.88 %
% 48.83/8.88 % clauses 4
% 48.83/8.88 % conjectures 1
% 48.83/8.88 % EPR 0
% 48.83/8.88 % Horn 4
% 48.83/8.88 % unary 1
% 48.83/8.88 % binary 2
% 48.83/8.88 % lits 8
% 48.83/8.88 % lits eq 8
% 48.83/8.88 % fd_pure 0
% 48.83/8.88 % fd_pseudo 0
% 48.83/8.88 % fd_cond 0
% 48.83/8.88 % fd_pseudo_cond 0
% 48.83/8.88 % AC symbols 0
% 48.83/8.88
% 48.83/8.88 % ------ Schedule dynamic 5 is on
% 48.83/8.88
% 48.83/8.88 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 48.83/8.88
% 48.83/8.88
% 48.83/8.88 % ------
% 48.83/8.88 % Current options:
% 48.83/8.88 % ------
% 48.83/8.88
% 48.83/8.88
% 48.83/8.88 %
% 48.83/8.88
% 48.83/8.88 % ------ Proving...
% 48.83/8.88 %
% 48.83/8.88
% 48.83/8.88 % SZS status Unsatisfiable for theBenchmark.p
% 48.83/8.88
% 48.83/8.88 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 48.83/8.88
% 48.83/8.88
%------------------------------------------------------------------------------