%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : GEO278+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 : n012.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 01:20:39 PM UTC 2026
% Result : Theorem 4.72s 2.03s
% Output : CNFRefutation 4.72s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named f41ERROR: Could not build tree for root c_20367ERROR: MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
( rcircle(vd1102)
& rcenter(vd1089,vd1102)
& ron(vd1096,vd1102) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','and(pred(comma_conjunct2(the(231)), 0), and(pred(comma_conjunct1(the(231)), 0), pred(the(231), 0)))') ).
fof(f5,axiom,
! [X0] :
( ( rline(X0)
& ron(vd1089,X0)
& ron(vd1085,X0) )
=> X0 = vskolem1099 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','replace(qu(theu(the(230), 1), imp(the(230))))') ).
fof(f6,axiom,
( rline(vskolem1099)
& ron(vd1089,vskolem1099)
& ron(vd1085,vskolem1099) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','replace(replace(and(pred(s2(plural(the(230))), 0), and(pred(s1(plural(the(230))), 0), pred(the(230), 0)))))') ).
fof(f7,axiom,
rR(vd1080,vd1089,vd1096),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','holds(conjunct2(comma_conjunct2(229)), 1097, 0)') ).
fof(f8,axiom,
rpoint(vd1096),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','pred(229, 0)') ).
fof(f9,axiom,
rpoint(vd1089),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','pred(226, 0)') ).
fof(f10,axiom,
? [X0] :
( rpoint(X0)
& vd1080 = X0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','qe(s1(plural(224)))') ).
fof(f137,plain,
? [X0] :
( rcircle(X0)
& rcenter(vd1089,X0)
& ron(vd1096,X0)
& vd1102 != X0 ),
inference(flattening,[],[f136]) ).
fof(f172,plain,
! [X0,X1,X2,X3,X4] :
( ! [X6] :
( ~ rpoint(X6)
| X0 != X6 )
| ! [X5] :
( ~ rpoint(X5)
| X1 != X5 )
| ~ rcenter(X2,X3)
| ~ rcenter(X2,X4)
| ~ ron(X0,X3)
| ~ ron(X1,X4)
| vf(X2,X0) != vf(X2,X1)
| X3 = X4 ),
inference(ennf_transformation,[],[f41]) ).
fof(f173,plain,
! [X0,X1,X2,X3,X4] :
( ! [X6] :
( ~ rpoint(X6)
| X0 != X6 )
| ! [X5] :
( ~ rpoint(X5)
| X1 != X5 )
| ~ rcenter(X2,X3)
| ~ rcenter(X2,X4)
| ~ ron(X0,X3)
| ~ ron(X1,X4)
| vf(X2,X0) != vf(X2,X1)
| X3 = X4 ),
inference(flattening,[],[f172]) ).
fof(f340,plain,
( rcircle(sK1)
& rcenter(vd1089,sK1)
& ron(vd1096,sK1)
& vd1102 != sK1 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(X0,sK1)],[f137]) ).
fof(f414,plain,
rcenter(vd1089,sK1),
inference(cnf_transformation,[],[f340]) ).
fof(f415,plain,
ron(vd1096,sK1),
inference(cnf_transformation,[],[f340]) ).
fof(f416,plain,
vd1102 != sK1,
inference(cnf_transformation,[],[f340]) ).
fof(f418,plain,
rcenter(vd1089,vd1102),
inference(cnf_transformation,[],[f3]) ).
fof(f419,plain,
ron(vd1096,vd1102),
inference(cnf_transformation,[],[f3]) ).
fof(f426,plain,
rpoint(vd1096),
inference(cnf_transformation,[],[f8]) ).
fof(f494,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ rpoint(X6)
| X0 != X6
| ~ rpoint(X5)
| X1 != X5
| ~ rcenter(X2,X3)
| ~ rcenter(X2,X4)
| ~ ron(X0,X3)
| ~ ron(X1,X4)
| vf(X2,X0) != vf(X2,X1)
| X3 = X4 ),
inference(cnf_transformation,[],[f173]) ).
fof(f817,plain,
! [X2,X3,X0,X6,X4,X5] :
( ~ rpoint(X6)
| X0 != X6
| ~ rpoint(X5)
| ~ rcenter(X2,X3)
| ~ rcenter(X2,X4)
| ~ ron(X0,X3)
| ~ ron(X5,X4)
| vf(X2,X0) != vf(X2,X5)
| X3 = X4 ),
inference(equality_resolution,[],[f494]) ).
fof(f818,plain,
! [X2,X3,X6,X4,X5] :
( ~ rpoint(X6)
| ~ rpoint(X5)
| ~ rcenter(X2,X3)
| ~ rcenter(X2,X4)
| ~ ron(X6,X3)
| ~ ron(X5,X4)
| vf(X2,X5) != vf(X2,X6)
| X3 = X4 ),
inference(equality_resolution,[],[f817]) ).
tcf(c_49,negated_conjecture,
vd1102 != sK1,
inference(cnf_transformation,[],[f416]) ).
tcf(c_50,negated_conjecture,
ron(vd1096,sK1),
inference(cnf_transformation,[],[f415]) ).
tcf(c_51,negated_conjecture,
rcenter(vd1089,sK1),
inference(cnf_transformation,[],[f414]) ).
tcf(c_53,plain,
ron(vd1096,vd1102),
inference(cnf_transformation,[],[f419]) ).
tcf(c_54,plain,
rcenter(vd1089,vd1102),
inference(cnf_transformation,[],[f418]) ).
tcf(c_61,plain,
rpoint(vd1096),
inference(cnf_transformation,[],[f426]) ).
tcf(c_124,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( ( X3 = X4 )
| ~ rpoint(X2)
| ~ rpoint(X1)
| ~ rcenter(X0,X4)
| ~ rcenter(X0,X3)
| ~ ron(X2,X4)
| ~ ron(X1,X3)
| ( vf(X0,X1) != vf(X0,X2) ) ),
inference(cnf_transformation,[],[f818]) ).
tcf(c_9250,plain,
! [X0_iProver_rpoint_1: iProver_rpoint_1,X0_iProver_rline_1: iProver_rline_1,X1_iProver_rpoint_1: iProver_rpoint_1,X1_iProver_rline_1: iProver_rline_1,X2_iProver_rpoint_1: iProver_rpoint_1] :
( ( X1_iProver_rline_1 = X0_iProver_rline_1 )
| ~ rpoint(X2_iProver_rpoint_1)
| ~ rpoint(X1_iProver_rpoint_1)
| ~ rcenter(X0_iProver_rpoint_1,X1_iProver_rline_1)
| ~ rcenter(X0_iProver_rpoint_1,X0_iProver_rline_1)
| ~ ron(X2_iProver_rpoint_1,X0_iProver_rline_1)
| ~ ron(X1_iProver_rpoint_1,X1_iProver_rline_1)
| ( vf(X0_iProver_rpoint_1,X1_iProver_rpoint_1) != vf(X0_iProver_rpoint_1,X2_iProver_rpoint_1) ) ),
inference(subtyping,[status(esa)],[c_124]) ).
tcf(c_9325,negated_conjecture,
vd1102 != sK1,
inference(subtyping,[status(esa)],[c_49]) ).
tcf(c_9346,plain,
! [X0_iProver_vplus_2: iProver_vplus_2] : X0_iProver_vplus_2 = X0_iProver_vplus_2,
theory(equality) ).
tcf(c_15620,plain,
! [X0_iProver_rpoint_1: iProver_rpoint_1,X1_iProver_rpoint_1: iProver_rpoint_1,X2_iProver_rpoint_1: iProver_rpoint_1] :
( ( vd1102 = sK1 )
| ~ rpoint(X2_iProver_rpoint_1)
| ~ rpoint(X1_iProver_rpoint_1)
| ~ rcenter(X0_iProver_rpoint_1,sK1)
| ~ rcenter(X0_iProver_rpoint_1,vd1102)
| ~ ron(X2_iProver_rpoint_1,sK1)
| ~ ron(X1_iProver_rpoint_1,vd1102)
| ( vf(X0_iProver_rpoint_1,X1_iProver_rpoint_1) != vf(X0_iProver_rpoint_1,X2_iProver_rpoint_1) ) ),
inference(instantiation,[status(thm)],[c_9250]) ).
tcf(c_15938,plain,
! [X0_iProver_rpoint_1: iProver_rpoint_1,X1_iProver_rpoint_1: iProver_rpoint_1] :
( ( vd1102 = sK1 )
| ~ rpoint(X1_iProver_rpoint_1)
| ~ rpoint(X0_iProver_rpoint_1)
| ~ rcenter(vd1089,sK1)
| ~ rcenter(vd1089,vd1102)
| ~ ron(X1_iProver_rpoint_1,sK1)
| ~ ron(X0_iProver_rpoint_1,vd1102)
| ( vf(vd1089,X0_iProver_rpoint_1) != vf(vd1089,X1_iProver_rpoint_1) ) ),
inference(instantiation,[status(thm)],[c_15620]) ).
tcf(c_16108,plain,
! [X0_iProver_rpoint_1: iProver_rpoint_1] :
( ( vd1102 = sK1 )
| ~ rpoint(vd1096)
| ~ rpoint(X0_iProver_rpoint_1)
| ~ rcenter(vd1089,sK1)
| ~ rcenter(vd1089,vd1102)
| ~ ron(vd1096,vd1102)
| ~ ron(X0_iProver_rpoint_1,sK1)
| ( vf(vd1089,vd1096) != vf(vd1089,X0_iProver_rpoint_1) ) ),
inference(instantiation,[status(thm)],[c_15938]) ).
tcf(c_17442,plain,
( ( vd1102 = sK1 )
| ~ rpoint(vd1096)
| ~ rcenter(vd1089,sK1)
| ~ rcenter(vd1089,vd1102)
| ~ ron(vd1096,sK1)
| ~ ron(vd1096,vd1102)
| ( vf(vd1089,vd1096) != vf(vd1089,vd1096) ) ),
inference(instantiation,[status(thm)],[c_16108]) ).
tcf(c_20366,plain,
vf(vd1089,vd1096) = vf(vd1089,vd1096),
inference(instantiation,[status(thm)],[c_9346]) ).
tcf(c_20367,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_20366,c_17442,c_9325,c_53,c_54,c_50,c_51,c_61]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : GEO278+1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.02 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.02/0.30 % Computer : n012.cluster.edu
% 0.02/0.30 % Model : x86_64 x86_64
% 0.02/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.02/0.30 % Memory : 8046.5625MB
% 0.02/0.30 % OS : Linux 6.8.0-71-generic
% 0.02/0.30 % CPULimit : 300
% 0.02/0.30 % WCLimit : 300
% 0.02/0.30 % DateTime : Wed Sep 23 11:47:52 UTC 2026
% 0.02/0.30 % CPUTime :
% 0.02/0.30 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.02/0.32 Running first-order theorem proving
% 0.02/0.32 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.02/0.33
% 0.02/0.33 % ======== iProver multi-core TPTP/SMT =========
% 0.02/0.33
% 0.06/0.33 % Detected problem language: tptp
% 0.06/0.34 % Proving...
% 4.72/2.03 % SZS status Started for theBenchmark.p
% 4.72/2.03 % SZS status Theorem for theBenchmark.p
% 4.72/2.03
% 4.72/2.03 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 4.72/2.03
% 4.72/2.03 % ------ iProver source info
% 4.72/2.03
% 4.72/2.03 % git: date: 2026-07-19 20:42:38 +0200
% 4.72/2.03 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 4.72/2.03 % git: non_committed_changes: false
% 4.72/2.03
% 4.72/2.03 % ------ Parsing...
% 4.72/2.03 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 4.72/2.03
% 4.72/2.03 % ------ 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 %
% 4.72/2.03
% 4.72/2.03 % ------ Preprocessing... gs_s sp: 14 0s gs_e snvd_s sp: 0 0s snvd_e %
% 4.72/2.03
% 4.72/2.03 % ------ Preprocessing... sf_s rm: 11 0s sf_e sf_s rm: 0 0s sf_e
% 4.72/2.03 % ------ Proving...
% 4.72/2.03 % ------ Problem Properties
% 4.72/2.03
% 4.72/2.03 %
% 4.72/2.03 % clauses 265
% 4.72/2.03 % conjectures 4
% 4.72/2.03 % EPR 83
% 4.72/2.03 % Horn 189
% 4.72/2.03 % unary 31
% 4.72/2.03 % binary 42
% 4.72/2.03 % lits 1484
% 4.72/2.03 % lits eq 172
% 4.72/2.03 % fd_pure 0
% 4.72/2.03 % fd_pseudo 0
% 4.72/2.03 % fd_cond 3
% 4.72/2.03 % fd_pseudo_cond 45
% 4.72/2.03 % AC symbols 0
% 4.72/2.03
% 4.72/2.03 % ------ Input Options Time Limit: Unbounded
% 4.72/2.03
% 4.72/2.03
% 4.72/2.03 % ------
% 4.72/2.03 % Current options:
% 4.72/2.03 % ------
% 4.72/2.03
% 4.72/2.03
% 4.72/2.03 %
% 4.72/2.03
% 4.72/2.03 % ------ Proving...
% 4.72/2.03 %
% 4.72/2.03
% 4.72/2.03 % SZS status Theorem for theBenchmark.p
% 4.72/2.03
% 4.72/2.03 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 4.72/2.03
% 4.72/2.03
%------------------------------------------------------------------------------