%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : GRP660+1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% Computer : n010.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:35:07 PM UTC 2026
% Result : Theorem 103.95s 17.48s
% Output : CNFRefutation 103.95s
% Verified :
% SZS Type : Refutation
% Derivation depth : 34
% Number of leaves : 6
% Syntax : Number of formulae : 99 ( 92 unt; 0 def)
% Number of atoms : 106 ( 105 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 19 ( 12 ~; 5 |; 2 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 3 avg)
% Maximal term depth : 6 ( 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 : 4 ( 4 usr; 0 con; 1-2 aty)
% Number of variables : 199 ( 0 sgn 196 !; 3 ?; 169 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] : mult(X1,ld(X1,X0)) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',f01) ).
fof(f2,axiom,
! [X0,X1] : ld(X1,mult(X1,X0)) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',f02) ).
fof(f3,axiom,
! [X0,X1] : mult(rd(X1,X0),X0) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',f03) ).
fof(f4,axiom,
! [X0,X1] : rd(mult(X1,X0),X0) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',f04) ).
fof(f5,axiom,
! [X0,X1,X2] : mult(mult(mult(X2,X1),X0),X2) = mult(X2,mult(X1,mult(X0,X2))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',f05) ).
fof(f6,conjecture,
? [X0] :
! [X1] :
( mult(X0,X1) = X1
& mult(X1,X0) = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goals) ).
fof(f7,negated_conjecture,
~ ? [X0] :
! [X1] :
( mult(X0,X1) = X1
& mult(X1,X0) = X1 ),
inference(negated_conjecture,[status(cth)],[f6]) ).
fof(f8,plain,
! [X0] :
? [X1] :
( mult(X0,X1) != X1
| mult(X1,X0) != X1 ),
inference(ennf_transformation,[],[f7]) ).
fof(f9,plain,
! [X0] :
( sK0(X0) != mult(X0,sK0(X0))
| sK0(X0) != mult(sK0(X0),X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(X1,sK0(X0))],[f8]) ).
fof(f10,plain,
! [X0,X1] : mult(X1,ld(X1,X0)) = X0,
inference(cnf_transformation,[],[f1]) ).
fof(f11,plain,
! [X0,X1] : ld(X1,mult(X1,X0)) = X0,
inference(cnf_transformation,[],[f2]) ).
fof(f12,plain,
! [X0,X1] : mult(rd(X1,X0),X0) = X1,
inference(cnf_transformation,[],[f3]) ).
fof(f13,plain,
! [X0,X1] : rd(mult(X1,X0),X0) = X1,
inference(cnf_transformation,[],[f4]) ).
fof(f14,plain,
! [X2,X0,X1] : mult(mult(mult(X2,X1),X0),X2) = mult(X2,mult(X1,mult(X0,X2))),
inference(cnf_transformation,[],[f5]) ).
fof(f15,plain,
! [X0] :
( sK0(X0) != mult(X0,sK0(X0))
| sK0(X0) != mult(sK0(X0),X0) ),
inference(cnf_transformation,[],[f9]) ).
tcf(c_49,plain,
! [X0: $i,X1: $i] : mult(X0,ld(X0,X1)) = X1,
inference(cnf_transformation,[],[f10]) ).
tcf(c_50,plain,
! [X0: $i,X1: $i] : ld(X0,mult(X0,X1)) = X1,
inference(cnf_transformation,[],[f11]) ).
tcf(c_51,plain,
! [X0: $i,X1: $i] : mult(rd(X0,X1),X1) = X0,
inference(cnf_transformation,[],[f12]) ).
tcf(c_52,plain,
! [X0: $i,X1: $i] : rd(mult(X0,X1),X1) = X0,
inference(cnf_transformation,[],[f13]) ).
tcf(c_53,plain,
! [X0: $i,X1: $i,X2: $i] : mult(mult(mult(X0,X1),X2),X0) = mult(X0,mult(X1,mult(X2,X0))),
inference(cnf_transformation,[],[f14]) ).
tcf(c_54,negated_conjecture,
! [X0: $i] :
( ( mult(X0,sK0(X0)) != sK0(X0) )
| ( mult(sK0(X0),X0) != sK0(X0) ) ),
inference(cnf_transformation,[],[f15]) ).
tcf(c_82,negated_conjecture,
! [X0: $i] :
( ( mult(X0,sK0(X0)) != sK0(X0) )
| ( mult(sK0(X0),X0) != sK0(X0) ) ),
inference(demodulation,[status(thm)],[c_54]) ).
tcf(c_130,plain,
! [X0: $i,X1: $i] : ld(rd(X0,X1),X0) = X1,
inference(superposition,[status(thm)],[c_51,c_50]) ).
tcf(c_132,plain,
! [X0: $i,X1: $i] : rd(X0,ld(X1,X0)) = X1,
inference(superposition,[status(thm)],[c_49,c_52]) ).
tcf(c_138,plain,
! [X0: $i,X1: $i,X2: $i] : mult(X0,mult(X1,mult(ld(mult(X0,X1),X2),X0))) = mult(X2,X0),
inference(superposition,[status(thm)],[c_49,c_53]) ).
tcf(c_140,plain,
! [X0: $i,X1: $i,X2: $i] : mult(X0,mult(ld(X0,X1),mult(X2,X0))) = mult(mult(X1,X2),X0),
inference(superposition,[status(thm)],[c_49,c_53]) ).
tcf(c_144,plain,
! [X0: $i,X1: $i,X2: $i] : rd(mult(X0,mult(X1,mult(X2,X0))),X0) = mult(mult(X0,X1),X2),
inference(superposition,[status(thm)],[c_53,c_52]) ).
tcf(c_162,plain,
! [X0: $i,X1: $i,X2: $i] : mult(X0,mult(ld(mult(X1,X0),X2),X1)) = ld(X1,mult(X2,X1)),
inference(superposition,[status(thm)],[c_138,c_50]) ).
tcf(c_185,plain,
! [X0: $i,X1: $i,X2: $i] : mult(mult(X0,rd(X1,X2)),X2) = mult(X2,mult(ld(X2,X0),X1)),
inference(superposition,[status(thm)],[c_51,c_140]) ).
tcf(c_226,plain,
! [X0: $i,X1: $i,X2: $i] : mult(mult(X0,rd(X1,mult(X2,X0))),X2) = rd(mult(X0,X1),X0),
inference(superposition,[status(thm)],[c_51,c_144]) ).
tcf(c_328,plain,
! [X0: $i,X1: $i,X2: $i] : ld(X0,ld(X1,mult(X2,X1))) = mult(ld(mult(X1,X0),X2),X1),
inference(superposition,[status(thm)],[c_162,c_50]) ).
tcf(c_390,plain,
! [X0: $i,X1: $i,X2: $i] : mult(X0,mult(ld(X0,rd(X1,rd(X2,X0))),X2)) = mult(X1,X0),
inference(superposition,[status(thm)],[c_51,c_185]) ).
tcf(c_602,plain,
! [X0: $i,X1: $i,X2: $i] : mult(X0,rd(X1,mult(X2,X0))) = rd(rd(mult(X0,X1),X0),X2),
inference(superposition,[status(thm)],[c_226,c_52]) ).
tcf(c_1098,plain,
! [X0: $i,X1: $i] : mult(ld(mult(X0,X1),X0),X0) = ld(X1,X0),
inference(superposition,[status(thm)],[c_50,c_328]) ).
tcf(c_1101,plain,
! [X0: $i,X1: $i,X2: $i] : mult(ld(mult(X0,X1),rd(X2,X0)),X0) = ld(X1,ld(X0,X2)),
inference(superposition,[status(thm)],[c_51,c_328]) ).
tcf(c_1168,plain,
! [X0: $i,X1: $i] : ld(mult(X0,X1),X0) = rd(ld(X1,X0),X0),
inference(superposition,[status(thm)],[c_1098,c_52]) ).
tcf(c_1169,plain,
! [X0: $i,X1: $i] : ld(ld(mult(X0,X1),X0),ld(X1,X0)) = X0,
inference(superposition,[status(thm)],[c_1098,c_50]) ).
tcf(c_1290,plain,
! [X0: $i,X1: $i] : ld(mult(X0,rd(X0,X1)),X0) = rd(X1,X0),
inference(superposition,[status(thm)],[c_130,c_1168]) ).
tcf(c_1332,plain,
! [X0: $i,X1: $i] : ld(ld(X0,rd(X0,X1)),ld(X1,rd(X0,X1))) = rd(X0,X1),
inference(superposition,[status(thm)],[c_51,c_1169]) ).
tcf(c_1473,plain,
! [X0: $i,X1: $i] : mult(X0,rd(X0,X1)) = rd(X0,rd(X1,X0)),
inference(superposition,[status(thm)],[c_1290,c_132]) ).
tcf(c_2011,plain,
! [X0: $i,X1: $i,X2: $i] : mult(ld(X0,rd(X1,rd(X2,X0))),X2) = ld(X0,mult(X1,X0)),
inference(superposition,[status(thm)],[c_390,c_50]) ).
tcf(c_2847,plain,
! [X0: $i,X1: $i,X2: $i] : mult(X0,rd(ld(X0,X1),mult(X2,X0))) = rd(rd(X1,X0),X2),
inference(superposition,[status(thm)],[c_49,c_602]) ).
tcf(c_3847,plain,
! [X0: $i,X1: $i,X2: $i] : ld(ld(X0,X1),ld(X0,X2)) = mult(ld(X1,rd(X2,X0)),X0),
inference(superposition,[status(thm)],[c_49,c_1101]) ).
tcf(c_4862,plain,
! [X0: $i,X1: $i,X2: $i] : ld(X0,rd(X1,rd(X2,X0))) = rd(ld(X0,mult(X1,X0)),X2),
inference(superposition,[status(thm)],[c_2011,c_52]) ).
tcf(c_5252,plain,
! [X0: $i,X1: $i,X2: $i] : mult(X0,rd(ld(X0,X1),X2)) = rd(rd(X1,X0),rd(X2,X0)),
inference(superposition,[status(thm)],[c_51,c_2847]) ).
tcf(c_6427,plain,
! [X0: $i,X1: $i,X2: $i] : mult(ld(X0,rd(mult(X1,X2),X1)),X1) = ld(ld(X1,X0),X2),
inference(superposition,[status(thm)],[c_50,c_3847]) ).
tcf(c_6458,plain,
! [X0: $i] : mult(ld(rd(X0,X0),rd(rd(X0,X0),X0)),X0) = rd(X0,X0),
inference(superposition,[status(thm)],[c_3847,c_1332]) ).
tcf(c_7635,plain,
! [X0: $i,X1: $i] : ld(mult(mult(X0,X1),X1),mult(X0,X1)) = ld(X1,rd(X0,rd(mult(X0,X1),X1))),
inference(superposition,[status(thm)],[c_4862,c_1168]) ).
tcf(c_7641,plain,
! [X0: $i,X1: $i] : ld(mult(mult(X0,X1),X1),mult(X0,X1)) = ld(X1,rd(X0,X0)),
inference(light_normalisation,[status(thm)],[c_7635,c_52]) ).
tcf(c_8593,plain,
! [X0: $i] : ld(rd(X0,X0),rd(rd(X0,X0),X0)) = rd(rd(X0,X0),X0),
inference(superposition,[status(thm)],[c_6458,c_52]) ).
tcf(c_9744,plain,
! [X0: $i,X1: $i] : ld(mult(X0,ld(X1,X0)),X0) = ld(ld(X1,X0),rd(X1,X1)),
inference(superposition,[status(thm)],[c_49,c_7641]) ).
tcf(c_10589,plain,
! [X0: $i] : mult(rd(X0,X0),rd(rd(X0,X0),X0)) = rd(rd(X0,X0),X0),
inference(superposition,[status(thm)],[c_8593,c_49]) ).
tcf(c_10702,plain,
! [X0: $i,X1: $i] : mult(ld(ld(X0,X1),rd(X0,X0)),X1) = ld(ld(X0,X1),X1),
inference(superposition,[status(thm)],[c_9744,c_1098]) ).
tcf(c_12878,plain,
! [X0: $i] : ld(rd(rd(X0,X0),X0),rd(X0,X0)) = rd(X0,rd(X0,X0)),
inference(superposition,[status(thm)],[c_10589,c_1290]) ).
tcf(c_13918,plain,
! [X0: $i,X1: $i] : ld(ld(X0,X1),rd(X0,X0)) = rd(ld(ld(X0,X1),X1),X1),
inference(superposition,[status(thm)],[c_10702,c_52]) ).
tcf(c_15251,plain,
! [X0: $i] : mult(X0,rd(X0,X0)) = X0,
inference(demodulation,[status(thm)],[c_12878,c_130,c_1473]) ).
tcf(c_15290,plain,
! [X0: $i,X1: $i] : ld(ld(X0,X1),rd(X0,X0)) = mult(ld(X1,rd(X0,X0)),X0),
inference(superposition,[status(thm)],[c_15251,c_6427]) ).
tcf(c_15319,plain,
! [X0: $i] : ld(X0,X0) = rd(X0,X0),
inference(superposition,[status(thm)],[c_15251,c_1290]) ).
tcf(c_15539,plain,
! [X0: $i] : mult(ld(X0,X0),X0) = X0,
inference(superposition,[status(thm)],[c_15319,c_51]) ).
tcf(c_15562,plain,
! [X0: $i,X1: $i] : ld(rd(X0,X1),rd(X0,X1)) = mult(X1,rd(ld(X1,X0),X0)),
inference(superposition,[status(thm)],[c_15319,c_5252]) ).
tcf(c_15563,plain,
! [X0: $i,X1: $i] : ld(rd(X0,X1),rd(X0,X1)) = mult(X1,ld(mult(X0,X1),X0)),
inference(light_normalisation,[status(thm)],[c_15562,c_1168]) ).
tcf(c_15690,plain,
! [X0: $i,X1: $i] : ld(ld(X0,X0),mult(X1,ld(X0,X0))) = mult(X0,mult(ld(X0,X1),ld(X0,X0))),
inference(superposition,[status(thm)],[c_15539,c_162]) ).
tcf(c_15985,plain,
! [X0: $i,X1: $i] : ld(ld(X0,X1),ld(X0,X0)) = rd(ld(ld(X0,X1),X1),X1),
inference(light_normalisation,[status(thm)],[c_13918,c_15319,c_15290]) ).
tcf(c_15986,plain,
! [X0: $i,X1: $i] : ld(mult(X0,ld(X1,X0)),X0) = mult(ld(X0,ld(X1,X1)),X1),
inference(demodulation,[status(thm)],[c_15985,c_1168,c_3847,c_15319]) ).
tcf(c_15988,plain,
! [X0: $i] : mult(ld(X0,ld(X0,X0)),X0) = ld(X0,X0),
inference(superposition,[status(thm)],[c_49,c_15986]) ).
tcf(c_16576,plain,
! [X0: $i] : ld(X0,ld(X0,X0)) = rd(ld(X0,X0),X0),
inference(superposition,[status(thm)],[c_15988,c_52]) ).
tcf(c_16800,plain,
! [X0: $i] : ld(mult(X0,X0),X0) = ld(X0,ld(X0,X0)),
inference(demodulation,[status(thm)],[c_16576,c_1168]) ).
tcf(c_30778,plain,
! [X0: $i] : ld(ld(X0,X0),ld(X0,X0)) = mult(X0,ld(mult(X0,X0),X0)),
inference(superposition,[status(thm)],[c_15319,c_15563]) ).
tcf(c_30850,plain,
! [X0: $i] : ld(ld(X0,X0),ld(X0,X0)) = mult(X0,ld(X0,ld(X0,X0))),
inference(light_normalisation,[status(thm)],[c_30778,c_16800]) ).
tcf(c_123508,plain,
! [X0: $i,X1: $i,X2: $i] : mult(X0,mult(X1,mult(ld(mult(X0,X1),X2),X0))) = mult(X2,X0),
inference(superposition,[status(thm)],[c_49,c_53]) ).
tcf(c_123510,plain,
! [X0: $i,X1: $i,X2: $i] : mult(X0,mult(ld(X0,X1),mult(X2,X0))) = mult(mult(X1,X2),X0),
inference(superposition,[status(thm)],[c_49,c_53]) ).
tcf(c_123515,plain,
! [X0: $i,X1: $i,X2: $i] : ld(mult(mult(X0,X1),X2),mult(X0,mult(X1,mult(X2,X0)))) = X0,
inference(superposition,[status(thm)],[c_53,c_50]) ).
tcf(c_123534,plain,
! [X0: $i,X1: $i,X2: $i] : mult(X0,mult(ld(mult(X1,X0),X2),X1)) = ld(X1,mult(X2,X1)),
inference(superposition,[status(thm)],[c_123508,c_50]) ).
tcf(c_123573,plain,
! [X0: $i,X1: $i,X2: $i] : ld(mult(X0,mult(X1,mult(X2,X0))),mult(mult(X0,X1),mult(X2,mult(X0,mult(X0,X1))))) = mult(X0,X1),
inference(superposition,[status(thm)],[c_53,c_123515]) ).
tcf(c_123609,plain,
! [X0: $i] : ld(ld(X0,X0),ld(X0,X0)) = ld(X0,X0),
inference(demodulation,[status(thm)],[c_30850,c_49]) ).
tcf(c_123610,plain,
! [X0: $i,X1: $i] : mult(ld(X0,X0),mult(ld(X0,X0),mult(X1,ld(X0,X0)))) = mult(mult(ld(X0,X0),X1),ld(X0,X0)),
inference(superposition,[status(thm)],[c_123609,c_123510]) ).
tcf(c_123611,plain,
! [X0: $i] : mult(ld(X0,X0),ld(X0,X0)) = ld(X0,X0),
inference(superposition,[status(thm)],[c_123609,c_49]) ).
tcf(c_123622,plain,
! [X0: $i,X1: $i] : mult(ld(X0,X0),mult(ld(ld(X0,X0),X1),ld(X0,X0))) = mult(mult(X1,ld(X0,X0)),ld(X0,X0)),
inference(superposition,[status(thm)],[c_123611,c_123510]) ).
tcf(c_123895,plain,
! [X0: $i] : mult(X0,mult(ld(X0,X0),ld(X0,X0))) = ld(ld(X0,X0),X0),
inference(superposition,[status(thm)],[c_49,c_15690]) ).
tcf(c_123899,plain,
! [X0: $i,X1: $i] : mult(ld(X0,X0),mult(ld(ld(X0,X0),X1),ld(X0,X0))) = ld(ld(X0,X0),mult(X1,ld(X0,X0))),
inference(superposition,[status(thm)],[c_123609,c_15690]) ).
tcf(c_123905,plain,
! [X0: $i] : ld(ld(X0,X0),X0) = mult(X0,ld(X0,X0)),
inference(light_normalisation,[status(thm)],[c_123895,c_123611]) ).
tcf(c_123907,plain,
! [X0: $i,X1: $i] : mult(mult(X0,ld(X1,X1)),ld(X1,X1)) = mult(X1,mult(ld(X1,X0),ld(X1,X1))),
inference(light_normalisation,[status(thm)],[c_123899,c_15690,c_123622]) ).
tcf(c_124034,plain,
! [X0: $i] : ld(ld(X0,X0),X0) = X0,
inference(demodulation,[status(thm)],[c_123905,c_49]) ).
tcf(c_124036,plain,
! [X0: $i] : mult(ld(X0,X0),X0) = X0,
inference(superposition,[status(thm)],[c_124034,c_49]) ).
tcf(c_124098,plain,
! [X0: $i,X1: $i,X2: $i] : ld(X0,ld(X1,mult(X2,X1))) = mult(ld(mult(X1,X0),X2),X1),
inference(superposition,[status(thm)],[c_123534,c_50]) ).
tcf(c_127613,plain,
! [X0: $i,X1: $i,X2: $i] : mult(ld(mult(X0,X1),rd(X2,X0)),X0) = ld(X1,ld(X0,X2)),
inference(superposition,[status(thm)],[c_51,c_124098]) ).
tcf(c_132399,plain,
! [X0: $i,X1: $i] : mult(ld(X0,rd(X1,ld(X0,X0))),ld(X0,X0)) = ld(X0,ld(ld(X0,X0),X1)),
inference(superposition,[status(thm)],[c_124036,c_127613]) ).
tcf(c_178960,plain,
! [X0: $i,X1: $i] : mult(X0,mult(ld(X0,rd(X1,ld(X0,X0))),ld(X0,X0))) = mult(X1,ld(X0,X0)),
inference(superposition,[status(thm)],[c_51,c_123907]) ).
tcf(c_179111,plain,
! [X0: $i,X1: $i] : mult(X0,ld(X0,ld(ld(X0,X0),X1))) = mult(X1,ld(X0,X0)),
inference(light_normalisation,[status(thm)],[c_178960,c_132399]) ).
tcf(c_179352,plain,
! [X0: $i,X1: $i] : ld(ld(X0,X0),X1) = mult(X1,ld(X0,X0)),
inference(demodulation,[status(thm)],[c_179111,c_49]) ).
tcf(c_179393,plain,
! [X0: $i,X1: $i] : mult(ld(X0,X0),mult(X1,ld(X0,X0))) = X1,
inference(superposition,[status(thm)],[c_179352,c_49]) ).
tcf(c_179394,plain,
! [X0: $i,X1: $i] : mult(mult(ld(X0,X0),X1),ld(X0,X0)) = X1,
inference(superposition,[status(thm)],[c_179352,c_50]) ).
tcf(c_179596,plain,
! [X0: $i,X1: $i] : mult(ld(X0,X0),mult(ld(X0,X0),mult(X1,ld(X0,X0)))) = X1,
inference(demodulation,[status(thm)],[c_123610,c_179394]) ).
tcf(c_180184,plain,
! [X0: $i,X1: $i] : ld(mult(ld(X0,X0),mult(ld(X0,X0),mult(X1,ld(X0,X0)))),mult(mult(ld(X0,X0),ld(X0,X0)),mult(X1,ld(X0,X0)))) = mult(ld(X0,X0),ld(X0,X0)),
inference(superposition,[status(thm)],[c_179393,c_123573]) ).
tcf(c_180263,plain,
! [X0: $i,X1: $i] : ld(X0,X0) = ld(X1,X1),
inference(light_normalisation,[status(thm)],[c_180184,c_123611,c_179393,c_179596]) ).
tcf(c_180901,plain,
! [X0: $i,X1: $i] : mult(X0,ld(X1,X1)) = X0,
inference(superposition,[status(thm)],[c_180263,c_49]) ).
tcf(c_180969,plain,
! [X0: $i,X1: $i] : mult(ld(X0,X0),X1) = X1,
inference(superposition,[status(thm)],[c_180263,c_124036]) ).
tcf(c_181215,plain,
! [X0: $i] : mult(ld(X0,X0),sK0(ld(X0,X0))) != sK0(ld(X0,X0)),
inference(superposition,[status(thm)],[c_180901,c_82]) ).
tcf(c_181277,plain,
$false,
inference(ground_joinability,[status(thm)],[c_181215,c_180969]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GRP660+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.08/0.36 % Computer : n010.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Wed Sep 23 15:32:57 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.36 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.12/0.40 Running first-order theorem proving
% 0.12/0.40 Running: /export/starexec/sandbox2/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.12/0.41
% 0.12/0.41 % ======== iProver multi-core TPTP/SMT =========
% 0.12/0.41
% 0.12/0.41 % Detected problem language: tptp
% 0.12/0.42 % Proving...
% 103.95/17.48 % SZS status Started for theBenchmark.p
% 103.95/17.48 % SZS status Theorem for theBenchmark.p
% 103.95/17.48
% 103.95/17.48 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 103.95/17.48
% 103.95/17.48 % ------ iProver source info
% 103.95/17.48
% 103.95/17.48 % git: date: 2026-07-19 20:42:38 +0200
% 103.95/17.48 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 103.95/17.48 % git: non_committed_changes: false
% 103.95/17.48
% 103.95/17.48 % ------ Parsing...
% 103.95/17.48 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 103.95/17.48
% 103.95/17.48 % ------ Preprocessing... sup_sim: 0 sf_s rm: 0 0s sf_e pe_s pe_e %
% 103.95/17.48
% 103.95/17.48 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 103.95/17.48
% 103.95/17.48 % ------ Preprocessing... sf_s rm: 0 0s sf_e
% 103.95/17.48 % ------ Proving...
% 103.95/17.48 % ------ Problem Properties
% 103.95/17.48
% 103.95/17.48 %
% 103.95/17.48 % clauses 6
% 103.95/17.48 % conjectures 1
% 103.95/17.48 % EPR 0
% 103.95/17.48 % Horn 6
% 103.95/17.48 % unary 5
% 103.95/17.48 % binary 1
% 103.95/17.48 % lits 7
% 103.95/17.48 % lits eq 7
% 103.95/17.48 % fd_pure 0
% 103.95/17.48 % fd_pseudo 0
% 103.95/17.48 % fd_cond 0
% 103.95/17.48 % fd_pseudo_cond 0
% 103.95/17.48 % AC symbols 0
% 103.95/17.48
% 103.95/17.48 % ------ Schedule dynamic 5 is on
% 103.95/17.48
% 103.95/17.48 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 103.95/17.48
% 103.95/17.48
% 103.95/17.48 % ------
% 103.95/17.48 % Current options:
% 103.95/17.48 % ------
% 103.95/17.48
% 103.95/17.48
% 103.95/17.48 %
% 103.95/17.48
% 103.95/17.48 % ------ Proving...
% 103.95/17.48 % Proof_search_loop: time out after: 2499 full_loop iterations
% 103.95/17.48
% 103.95/17.48 % ------ Input Options"1. --res_lit_sel adaptive --res_lit_sel_side num_symb" Time Limit: 15.
% 103.95/17.48
% 103.95/17.48
% 103.95/17.48 % ------
% 103.95/17.48 % Current options:
% 103.95/17.48 % ------
% 103.95/17.48
% 103.95/17.48
% 103.95/17.48 %
% 103.95/17.48
% 103.95/17.48 % ------ Proving...
% 103.95/17.48 %
% 103.95/17.48
% 103.95/17.48 % SZS status Theorem for theBenchmark.p
% 103.95/17.48
% 103.95/17.48 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 103.95/17.48
% 103.95/17.48
%------------------------------------------------------------------------------