%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : GEO332+1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% Computer : n013.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:20:58 PM UTC 2026
% Result : Theorem 130.04s 20.98s
% Output : CNFRefutation 130.04s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named f131ERROR: Could not build tree for root c_78653ERROR: MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
rless(vf(vd1361,vd1363),vf(vd1361,vd1362)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','holds(389, 1370, 0)') ).
fof(f4,axiom,
vf(vd1361,vd1362) != vf(vd1361,vd1363),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','holds(387, 1369, 0)') ).
fof(f5,axiom,
vangle(vd1361,vd1362,vd1363) = vangle(vd1361,vd1363,vd1362),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','holds(386, 1365, 0)') ).
fof(f6,axiom,
vd1362 != vd1363,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','pred(386, 9)') ).
fof(f7,axiom,
vd1361 != vd1363,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','pred(386, 8)') ).
fof(f8,axiom,
vd1361 != vd1362,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','pred(386, 7)') ).
fof(f9,axiom,
? [X0] :
( rpoint(X0)
& vd1363 = X0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','qe(s3(plural(386)))') ).
fof(f10,axiom,
? [X0] :
( rpoint(X0)
& vd1362 = X0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','qe(s2(plural(386)))') ).
fof(f11,axiom,
? [X0] :
( rpoint(X0)
& vd1361 = X0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','qe(s1(plural(386)))') ).
fof(f142,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( ~ rpoint(X1)
| X0 != X1
| ~ rpoint(X3)
| X2 != X3
| ~ rpoint(X5)
| X4 != X5
| ~ rpoint(X7)
| X6 != X7
| X0 = X2
| X4 = X6
| ~ rless(vf(X4,X6),vf(X0,X2))
| vf(X0,vskolem1120(X0,X1,X2,X3,X4,X5,X6,X7)) = vf(X4,X6) ),
inference(ennf_transformation,[],[f17]) ).
fof(f143,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( ~ rpoint(X1)
| X0 != X1
| ~ rpoint(X3)
| X2 != X3
| ~ rpoint(X5)
| X4 != X5
| ~ rpoint(X7)
| X6 != X7
| X0 = X2
| X4 = X6
| ~ rless(vf(X4,X6),vf(X0,X2))
| vf(X0,vskolem1120(X0,X1,X2,X3,X4,X5,X6,X7)) = vf(X4,X6) ),
inference(flattening,[],[f142]) ).
fof(f144,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( ~ rpoint(X1)
| X0 != X1
| ~ rpoint(X3)
| X2 != X3
| ~ rpoint(X5)
| X4 != X5
| ~ rpoint(X7)
| X6 != X7
| X0 = X2
| X4 = X6
| ~ rless(vf(X4,X6),vf(X0,X2))
| rR(vskolem1120(X0,X1,X2,X3,X4,X5,X6,X7),X0,X2) ),
inference(ennf_transformation,[],[f18]) ).
fof(f145,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( ~ rpoint(X1)
| X0 != X1
| ~ rpoint(X3)
| X2 != X3
| ~ rpoint(X5)
| X4 != X5
| ~ rpoint(X7)
| X6 != X7
| X0 = X2
| X4 = X6
| ~ rless(vf(X4,X6),vf(X0,X2))
| rR(vskolem1120(X0,X1,X2,X3,X4,X5,X6,X7),X0,X2) ),
inference(flattening,[],[f144]) ).
fof(f146,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( ~ rpoint(X1)
| X0 != X1
| ~ rpoint(X3)
| X2 != X3
| ~ rpoint(X5)
| X4 != X5
| ~ rpoint(X7)
| X6 != X7
| X0 = X2
| X4 = X6
| ~ rless(vf(X4,X6),vf(X0,X2))
| rpoint(vskolem1120(X0,X1,X2,X3,X4,X5,X6,X7)) ),
inference(ennf_transformation,[],[f19]) ).
fof(f147,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( ~ rpoint(X1)
| X0 != X1
| ~ rpoint(X3)
| X2 != X3
| ~ rpoint(X5)
| X4 != X5
| ~ rpoint(X7)
| X6 != X7
| X0 = X2
| X4 = X6
| ~ rless(vf(X4,X6),vf(X0,X2))
| rpoint(vskolem1120(X0,X1,X2,X3,X4,X5,X6,X7)) ),
inference(flattening,[],[f146]) ).
fof(f160,plain,
! [X0,X1] :
( ! [X3] :
( ~ rpoint(X3)
| X0 != X3 )
| ! [X2] :
( ~ rpoint(X2)
| X1 != X2 )
| vf(X0,X1) = vf(X1,X0) ),
inference(ennf_transformation,[],[f26]) ).
fof(f161,plain,
! [X0,X1] :
( ! [X3] :
( ~ rpoint(X3)
| X0 != X3 )
| ! [X2] :
( ~ rpoint(X2)
| X1 != X2 )
| vf(X0,X1) = vf(X1,X0) ),
inference(flattening,[],[f160]) ).
fof(f348,plain,
( rpoint(sK1)
& vd1363 = sK1 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(X0,sK1)],[f9]) ).
fof(f349,plain,
( rpoint(sK2)
& vd1362 = sK2 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2]),skolemize(X0,sK2)],[f10]) ).
fof(f350,plain,
( rpoint(sK3)
& vd1361 = sK3 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3]),skolemize(X0,sK3)],[f11]) ).
fof(f428,plain,
! [X0] :
( ~ rpoint(X0)
| ~ rR(X0,vd1362,vd1361)
| vf(vd1362,X0) != vf(vd1361,vd1363) ),
inference(cnf_transformation,[],[f131]) ).
fof(f429,plain,
rless(vf(vd1361,vd1363),vf(vd1361,vd1362)),
inference(cnf_transformation,[],[f3]) ).
fof(f433,plain,
vd1361 != vd1363,
inference(cnf_transformation,[],[f7]) ).
fof(f434,plain,
vd1362 != vd1361,
inference(cnf_transformation,[],[f8]) ).
fof(f435,plain,
rpoint(sK1),
inference(cnf_transformation,[],[f348]) ).
fof(f436,plain,
vd1363 = sK1,
inference(cnf_transformation,[],[f348]) ).
fof(f437,plain,
rpoint(sK2),
inference(cnf_transformation,[],[f349]) ).
fof(f438,plain,
vd1362 = sK2,
inference(cnf_transformation,[],[f349]) ).
fof(f439,plain,
rpoint(sK3),
inference(cnf_transformation,[],[f350]) ).
fof(f440,plain,
vd1361 = sK3,
inference(cnf_transformation,[],[f350]) ).
fof(f455,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ rpoint(X1)
| X0 != X1
| ~ rpoint(X3)
| X2 != X3
| ~ rpoint(X5)
| X4 != X5
| ~ rpoint(X7)
| X6 != X7
| X0 = X2
| X4 = X6
| ~ rless(vf(X4,X6),vf(X0,X2))
| vf(X4,X6) = vf(X0,vskolem1120(X0,X1,X2,X3,X4,X5,X6,X7)) ),
inference(cnf_transformation,[],[f143]) ).
fof(f456,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ rpoint(X1)
| X0 != X1
| ~ rpoint(X3)
| X2 != X3
| ~ rpoint(X5)
| X4 != X5
| ~ rpoint(X7)
| X6 != X7
| X0 = X2
| X4 = X6
| ~ rless(vf(X4,X6),vf(X0,X2))
| rR(vskolem1120(X0,X1,X2,X3,X4,X5,X6,X7),X0,X2) ),
inference(cnf_transformation,[],[f145]) ).
fof(f457,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ rpoint(X1)
| X0 != X1
| ~ rpoint(X3)
| X2 != X3
| ~ rpoint(X5)
| X4 != X5
| ~ rpoint(X7)
| X6 != X7
| X0 = X2
| X4 = X6
| ~ rless(vf(X4,X6),vf(X0,X2))
| rpoint(vskolem1120(X0,X1,X2,X3,X4,X5,X6,X7)) ),
inference(cnf_transformation,[],[f147]) ).
fof(f470,plain,
! [X2,X3,X0,X1] :
( ~ rpoint(X3)
| X0 != X3
| ~ rpoint(X2)
| X1 != X2
| vf(X0,X1) = vf(X1,X0) ),
inference(cnf_transformation,[],[f161]) ).
fof(f688,plain,
! [X0] :
( ~ rpoint(X0)
| ~ rR(X0,sK2,sK3)
| vf(sK2,X0) != vf(sK3,sK1) ),
inference(definition_unfolding,[],[f428,f438,f440,f436,f438,f440]) ).
fof(f689,plain,
rless(vf(sK3,sK1),vf(sK3,sK2)),
inference(definition_unfolding,[],[f429,f440,f436,f440,f438]) ).
fof(f693,plain,
sK1 != sK3,
inference(definition_unfolding,[],[f433,f440,f436]) ).
fof(f694,plain,
sK2 != sK3,
inference(definition_unfolding,[],[f434,f438,f440]) ).
fof(f786,plain,
! [X2,X3,X0,X1,X7,X4,X5] :
( ~ rpoint(X1)
| X0 != X1
| ~ rpoint(X3)
| X2 != X3
| ~ rpoint(X5)
| X4 != X5
| ~ rpoint(X7)
| X0 = X2
| X4 = X7
| ~ rless(vf(X4,X7),vf(X0,X2))
| vf(X4,X7) = vf(X0,vskolem1120(X0,X1,X2,X3,X4,X5,X7,X7)) ),
inference(equality_resolution,[],[f455]) ).
fof(f787,plain,
! [X2,X3,X0,X1,X7,X5] :
( ~ rpoint(X1)
| X0 != X1
| ~ rpoint(X3)
| X2 != X3
| ~ rpoint(X5)
| ~ rpoint(X7)
| X0 = X2
| X5 = X7
| ~ rless(vf(X5,X7),vf(X0,X2))
| vf(X5,X7) = vf(X0,vskolem1120(X0,X1,X2,X3,X5,X5,X7,X7)) ),
inference(equality_resolution,[],[f786]) ).
fof(f788,plain,
! [X3,X0,X1,X7,X5] :
( ~ rpoint(X1)
| X0 != X1
| ~ rpoint(X3)
| ~ rpoint(X5)
| ~ rpoint(X7)
| X0 = X3
| X5 = X7
| ~ rless(vf(X5,X7),vf(X0,X3))
| vf(X5,X7) = vf(X0,vskolem1120(X0,X1,X3,X3,X5,X5,X7,X7)) ),
inference(equality_resolution,[],[f787]) ).
fof(f789,plain,
! [X3,X1,X7,X5] :
( ~ rpoint(X1)
| ~ rpoint(X3)
| ~ rpoint(X5)
| ~ rpoint(X7)
| X1 = X3
| X5 = X7
| ~ rless(vf(X5,X7),vf(X1,X3))
| vf(X5,X7) = vf(X1,vskolem1120(X1,X1,X3,X3,X5,X5,X7,X7)) ),
inference(equality_resolution,[],[f788]) ).
fof(f790,plain,
! [X2,X3,X0,X1,X7,X4,X5] :
( ~ rpoint(X1)
| X0 != X1
| ~ rpoint(X3)
| X2 != X3
| ~ rpoint(X5)
| X4 != X5
| ~ rpoint(X7)
| X0 = X2
| X4 = X7
| ~ rless(vf(X4,X7),vf(X0,X2))
| rR(vskolem1120(X0,X1,X2,X3,X4,X5,X7,X7),X0,X2) ),
inference(equality_resolution,[],[f456]) ).
fof(f791,plain,
! [X2,X3,X0,X1,X7,X5] :
( ~ rpoint(X1)
| X0 != X1
| ~ rpoint(X3)
| X2 != X3
| ~ rpoint(X5)
| ~ rpoint(X7)
| X0 = X2
| X5 = X7
| ~ rless(vf(X5,X7),vf(X0,X2))
| rR(vskolem1120(X0,X1,X2,X3,X5,X5,X7,X7),X0,X2) ),
inference(equality_resolution,[],[f790]) ).
fof(f792,plain,
! [X3,X0,X1,X7,X5] :
( ~ rpoint(X1)
| X0 != X1
| ~ rpoint(X3)
| ~ rpoint(X5)
| ~ rpoint(X7)
| X0 = X3
| X5 = X7
| ~ rless(vf(X5,X7),vf(X0,X3))
| rR(vskolem1120(X0,X1,X3,X3,X5,X5,X7,X7),X0,X3) ),
inference(equality_resolution,[],[f791]) ).
fof(f793,plain,
! [X3,X1,X7,X5] :
( ~ rpoint(X1)
| ~ rpoint(X3)
| ~ rpoint(X5)
| ~ rpoint(X7)
| X1 = X3
| X5 = X7
| ~ rless(vf(X5,X7),vf(X1,X3))
| rR(vskolem1120(X1,X1,X3,X3,X5,X5,X7,X7),X1,X3) ),
inference(equality_resolution,[],[f792]) ).
fof(f794,plain,
! [X2,X3,X0,X1,X7,X4,X5] :
( ~ rpoint(X1)
| X0 != X1
| ~ rpoint(X3)
| X2 != X3
| ~ rpoint(X5)
| X4 != X5
| ~ rpoint(X7)
| X0 = X2
| X4 = X7
| ~ rless(vf(X4,X7),vf(X0,X2))
| rpoint(vskolem1120(X0,X1,X2,X3,X4,X5,X7,X7)) ),
inference(equality_resolution,[],[f457]) ).
fof(f795,plain,
! [X2,X3,X0,X1,X7,X5] :
( ~ rpoint(X1)
| X0 != X1
| ~ rpoint(X3)
| X2 != X3
| ~ rpoint(X5)
| ~ rpoint(X7)
| X0 = X2
| X5 = X7
| ~ rless(vf(X5,X7),vf(X0,X2))
| rpoint(vskolem1120(X0,X1,X2,X3,X5,X5,X7,X7)) ),
inference(equality_resolution,[],[f794]) ).
fof(f796,plain,
! [X3,X0,X1,X7,X5] :
( ~ rpoint(X1)
| X0 != X1
| ~ rpoint(X3)
| ~ rpoint(X5)
| ~ rpoint(X7)
| X0 = X3
| X5 = X7
| ~ rless(vf(X5,X7),vf(X0,X3))
| rpoint(vskolem1120(X0,X1,X3,X3,X5,X5,X7,X7)) ),
inference(equality_resolution,[],[f795]) ).
fof(f797,plain,
! [X3,X1,X7,X5] :
( ~ rpoint(X1)
| ~ rpoint(X3)
| ~ rpoint(X5)
| ~ rpoint(X7)
| X1 = X3
| X5 = X7
| ~ rless(vf(X5,X7),vf(X1,X3))
| rpoint(vskolem1120(X1,X1,X3,X3,X5,X5,X7,X7)) ),
inference(equality_resolution,[],[f796]) ).
fof(f842,plain,
! [X2,X3,X0] :
( ~ rpoint(X3)
| X0 != X3
| ~ rpoint(X2)
| vf(X0,X2) = vf(X2,X0) ),
inference(equality_resolution,[],[f470]) ).
fof(f843,plain,
! [X2,X3] :
( ~ rpoint(X3)
| ~ rpoint(X2)
| vf(X3,X2) = vf(X2,X3) ),
inference(equality_resolution,[],[f842]) ).
tcf(c_49,negated_conjecture,
! [X0: $i] :
( ~ rpoint(X0)
| ~ rR(X0,sK2,sK3)
| ( vf(sK2,X0) != vf(sK3,sK1) ) ),
inference(cnf_transformation,[],[f688]) ).
tcf(c_50,plain,
rless(vf(sK3,sK1),vf(sK3,sK2)),
inference(cnf_transformation,[],[f689]) ).
tcf(c_54,plain,
sK3 != sK1,
inference(cnf_transformation,[],[f693]) ).
tcf(c_55,plain,
sK2 != sK3,
inference(cnf_transformation,[],[f694]) ).
tcf(c_56,plain,
rpoint(sK1),
inference(cnf_transformation,[],[f435]) ).
tcf(c_57,plain,
rpoint(sK2),
inference(cnf_transformation,[],[f437]) ).
tcf(c_58,plain,
rpoint(sK3),
inference(cnf_transformation,[],[f439]) ).
tcf(c_73,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( X2 = X3 )
| ( X0 = X1 )
| ( vf(X2,vskolem1120(X2,X2,X3,X3,X0,X0,X1,X1)) = vf(X0,X1) )
| ~ rpoint(X3)
| ~ rpoint(X2)
| ~ rpoint(X1)
| ~ rpoint(X0)
| ~ rless(vf(X0,X1),vf(X2,X3)) ),
inference(cnf_transformation,[],[f789]) ).
tcf(c_74,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( rR(vskolem1120(X2,X2,X3,X3,X0,X0,X1,X1),X2,X3)
| ( X2 = X3 )
| ( X0 = X1 )
| ~ rpoint(X3)
| ~ rpoint(X2)
| ~ rpoint(X1)
| ~ rpoint(X0)
| ~ rless(vf(X0,X1),vf(X2,X3)) ),
inference(cnf_transformation,[],[f793]) ).
tcf(c_75,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( rpoint(vskolem1120(X2,X2,X3,X3,X0,X0,X1,X1))
| ( X2 = X3 )
| ( X0 = X1 )
| ~ rpoint(X3)
| ~ rpoint(X2)
| ~ rpoint(X1)
| ~ rpoint(X0)
| ~ rless(vf(X0,X1),vf(X2,X3)) ),
inference(cnf_transformation,[],[f797]) ).
tcf(c_88,plain,
! [X0: $i,X1: $i] :
( ( vf(X0,X1) = vf(X1,X0) )
| ~ rpoint(X1)
| ~ rpoint(X0) ),
inference(cnf_transformation,[],[f843]) ).
tcf(c_10148,plain,
! [X0: $i] : X0 = X0,
theory(equality) ).
tcf(c_10154,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( rless(X0,X2)
| ~ rless(X1,X3)
| ( X2 != X3 )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_17728,plain,
! [X0: $i] :
( ( vf(X0,sK2) = vf(sK2,X0) )
| ~ rpoint(X0) ),
inference(superposition,[status(thm)],[c_57,c_88]) ).
tcf(c_18275,plain,
vf(sK2,sK3) = vf(sK3,sK2),
inference(superposition,[status(thm)],[c_58,c_17728]) ).
tcf(c_24474,plain,
vf(sK3,sK1) = vf(sK3,sK1),
inference(instantiation,[status(thm)],[c_10148]) ).
tcf(c_58866,plain,
! [X0: $i,X1: $i] :
( rless(X0,X1)
| ~ rless(vf(sK3,sK1),vf(sK3,sK2))
| ( X1 != vf(sK3,sK2) )
| ( X0 != vf(sK3,sK1) ) ),
inference(instantiation,[status(thm)],[c_10154]) ).
tcf(c_60064,plain,
! [X0: $i,X1: $i,X2: $i] :
( rless(X2,vf(X0,X1))
| ~ rless(vf(sK3,sK1),vf(sK3,sK2))
| ( X2 != vf(sK3,sK1) )
| ( vf(X0,X1) != vf(sK3,sK2) ) ),
inference(instantiation,[status(thm)],[c_58866]) ).
tcf(c_63891,plain,
! [X0: $i] :
( rless(X0,vf(sK2,sK3))
| ~ rless(vf(sK3,sK1),vf(sK3,sK2))
| ( X0 != vf(sK3,sK1) )
| ( vf(sK2,sK3) != vf(sK3,sK2) ) ),
inference(instantiation,[status(thm)],[c_60064]) ).
tcf(c_65616,plain,
( rless(vf(sK3,sK1),vf(sK2,sK3))
| ~ rless(vf(sK3,sK1),vf(sK3,sK2))
| ( vf(sK3,sK1) != vf(sK3,sK1) )
| ( vf(sK2,sK3) != vf(sK3,sK2) ) ),
inference(instantiation,[status(thm)],[c_63891]) ).
tcf(c_69086,plain,
( ( sK3 = sK1 )
| ( sK2 = sK3 )
| ( vf(sK2,vskolem1120(sK2,sK2,sK3,sK3,sK3,sK3,sK1,sK1)) = vf(sK3,sK1) )
| ~ rpoint(sK1)
| ~ rpoint(sK3)
| ~ rpoint(sK2)
| ~ rless(vf(sK3,sK1),vf(sK2,sK3)) ),
inference(instantiation,[status(thm)],[c_73]) ).
tcf(c_69087,plain,
( rR(vskolem1120(sK2,sK2,sK3,sK3,sK3,sK3,sK1,sK1),sK2,sK3)
| ( sK3 = sK1 )
| ( sK2 = sK3 )
| ~ rpoint(sK1)
| ~ rpoint(sK3)
| ~ rpoint(sK2)
| ~ rless(vf(sK3,sK1),vf(sK2,sK3)) ),
inference(instantiation,[status(thm)],[c_74]) ).
tcf(c_69088,plain,
( rpoint(vskolem1120(sK2,sK2,sK3,sK3,sK3,sK3,sK1,sK1))
| ( sK3 = sK1 )
| ( sK2 = sK3 )
| ~ rpoint(sK1)
| ~ rpoint(sK3)
| ~ rpoint(sK2)
| ~ rless(vf(sK3,sK1),vf(sK2,sK3)) ),
inference(instantiation,[status(thm)],[c_75]) ).
tcf(c_78652,plain,
( ~ rpoint(vskolem1120(sK2,sK2,sK3,sK3,sK3,sK3,sK1,sK1))
| ~ rR(vskolem1120(sK2,sK2,sK3,sK3,sK3,sK3,sK1,sK1),sK2,sK3)
| ( vf(sK2,vskolem1120(sK2,sK2,sK3,sK3,sK3,sK3,sK1,sK1)) != vf(sK3,sK1) ) ),
inference(instantiation,[status(thm)],[c_49]) ).
tcf(c_78653,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_78652,c_69086,c_69087,c_69088,c_65616,c_24474,c_18275,c_50,c_54,c_55,c_56,c_57,c_58]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GEO332+1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.11/0.36 % Computer : n013.cluster.edu
% 0.11/0.36 % Model : x86_64 x86_64
% 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.36 % Memory : 8046.5625MB
% 0.11/0.36 % OS : Linux 6.8.0-71-generic
% 0.11/0.36 % CPULimit : 300
% 0.11/0.36 % WCLimit : 300
% 0.11/0.36 % DateTime : Wed Sep 23 11:57:06 UTC 2026
% 0.11/0.36 % CPUTime :
% 0.11/0.36 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.11/0.40 Running first-order theorem proving
% 0.11/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.11/0.41
% 0.11/0.41 % ======== iProver multi-core TPTP/SMT =========
% 0.11/0.41
% 0.11/0.41 % Detected problem language: tptp
% 0.11/0.42 % Proving...
% 130.04/20.98 % SZS status Started for theBenchmark.p
% 130.04/20.98 % SZS status Theorem for theBenchmark.p
% 130.04/20.98
% 130.04/20.98 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 130.04/20.98
% 130.04/20.98 % ------ iProver source info
% 130.04/20.98
% 130.04/20.98 % git: date: 2026-07-19 20:42:38 +0200
% 130.04/20.98 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 130.04/20.98 % git: non_committed_changes: false
% 130.04/20.98
% 130.04/20.98 % ------ Parsing...
% 130.04/20.98 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 130.04/20.98
% 130.04/20.98 % ------ Preprocessing... sup_sim: 0 sf_s rm: 1 0s sf_e pe_s pe_e sup_sim: 0 sf_s rm: 1 0s sf_e pe_s pe_e %
% 130.04/20.98
% 130.04/20.98 % ------ Preprocessing... gs_s sp: 14 0s gs_e snvd_s sp: 0 0s snvd_e %
% 130.04/20.98
% 130.04/20.98 % ------ Preprocessing... sf_s rm: 3 0s sf_e sf_s rm: 0 0s sf_e
% 130.04/20.98 % ------ Proving...
% 130.04/20.98 % ------ Problem Properties
% 130.04/20.98
% 130.04/20.98 %
% 130.04/20.98 % clauses 262
% 130.04/20.98 % conjectures 1
% 130.04/20.98 % EPR 59
% 130.04/20.98 % Horn 167
% 130.04/20.98 % unary 11
% 130.04/20.98 % binary 42
% 130.04/20.98 % lits 1685
% 130.04/20.98 % lits eq 277
% 130.04/20.98 % fd_pure 0
% 130.04/20.98 % fd_pseudo 0
% 130.04/20.98 % fd_cond 0
% 130.04/20.98 % fd_pseudo_cond 64
% 130.04/20.98 % AC symbols 0
% 130.04/20.98
% 130.04/20.98 % ------ Input Options Time Limit: Unbounded
% 130.04/20.98
% 130.04/20.98
% 130.04/20.98 % ------
% 130.04/20.98 % Current options:
% 130.04/20.98 % ------
% 130.04/20.98
% 130.04/20.98
% 130.04/20.98 %
% 130.04/20.98
% 130.04/20.98 % ------ Proving...
% 130.04/20.98 %
% 130.04/20.98
% 130.04/20.98 % SZS status Theorem for theBenchmark.p
% 130.04/20.98
% 130.04/20.98 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 130.04/20.98
% 130.04/20.98
%------------------------------------------------------------------------------