%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : GEO169+1 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 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 : Sun Sep 27 07:14:20 AM UTC 2026
% Result : Theorem 136.74s 17.91s
% Output : CNFRefutation 136.74s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats ran out of CPU time)
% Comments :
%------------------------------------------------------------------------------
fof(goal_normal,axiom,
! [X0] :
( ( incident(ab,X0)
& incident(ac,X0)
& incident(bc,X0)
& 'line$uequal'(X0,X0) )
=> goal ) ).
fof(t1in2,axiom,
( ( incident(c1,a2b2)
& incident(b1,a2c2)
& incident(a1,b2c2) )
=> goal ) ).
fof(t2in1,axiom,
( ( incident(c2,a1b1)
& incident(b2,a1c1)
& incident(a2,b1c1) )
=> goal ) ).
fof(gap_a,axiom,
( incident(b2,a1c1)
| incident(a1,b2c2) ) ).
fof(gap_b,axiom,
( incident(c2,a1b1)
| incident(b1,a2c2) ) ).
fof(gap_c,axiom,
( incident(a2,b1c1)
| incident(c1,a2b2) ) ).
fof(ia1b1,axiom,
incident(a1,a1b1) ).
fof(ib1a1,axiom,
incident(b1,a1b1) ).
fof(ia2b2,axiom,
incident(a2,a2b2) ).
fof(ib2a2,axiom,
incident(b2,a2b2) ).
fof(ia1c1,axiom,
incident(a1,a1c1) ).
fof(ic1a1,axiom,
incident(c1,a1c1) ).
fof(ia2c2,axiom,
incident(a2,a2c2) ).
fof(ic2a2,axiom,
incident(c2,a2c2) ).
fof(ic1b1,axiom,
incident(c1,b1c1) ).
fof(ib1c1,axiom,
incident(b1,b1c1) ).
fof(ic2b2,axiom,
incident(c2,b2c2) ).
fof(ib2c2,axiom,
incident(b2,b2c2) ).
fof(iooa,axiom,
incident(o,oa) ).
fof(ioob,axiom,
incident(o,ob) ).
fof(iooc,axiom,
incident(o,oc) ).
fof(ia1oa,axiom,
incident(a1,oa) ).
fof(ia2oa,axiom,
incident(a2,oa) ).
fof(ib1ob,axiom,
incident(b1,ob) ).
fof(ib2ob,axiom,
incident(b2,ob) ).
fof(ic1oc,axiom,
incident(c1,oc) ).
fof(ic2oc,axiom,
incident(c2,oc) ).
fof(ibc1,axiom,
incident(bc,b1c1) ).
fof(ibc2,axiom,
incident(bc,b2c2) ).
fof(iac1,axiom,
incident(ac,a1c1) ).
fof(iac2,axiom,
incident(ac,a2c2) ).
fof(iab1,axiom,
incident(ab,a1b1) ).
fof(iab2,axiom,
incident(ab,a2b2) ).
fof(triangle1,axiom,
! [X0] :
( ( incident(c1,X0)
& incident(b1,X0)
& incident(a1,X0) )
=> goal ) ).
fof(triangle2,axiom,
! [X0] :
( ( incident(c2,X0)
& incident(b2,X0)
& incident(a2,X0) )
=> goal ) ).
fof(notaa,axiom,
( 'point$uequal'(a2,a1)
=> goal ) ).
fof(notbb,axiom,
( 'point$uequal'(b2,b1)
=> goal ) ).
fof(notcc,axiom,
( 'point$uequal'(c2,c1)
=> goal ) ).
fof(notbc,axiom,
( 'line$uequal'(b1c1,b2c2)
=> goal ) ).
fof(notac,axiom,
( 'line$uequal'(a1c1,a2c2)
=> goal ) ).
fof(notab,axiom,
( 'line$uequal'(a1b1,a2b2)
=> goal ) ).
fof(symmetry_of_point_equal,axiom,
! [X0,X1] :
( 'point$uequal'(X0,X1)
=> 'point$uequal'(X1,X0) ) ).
fof(transitivity_of_point_equal,axiom,
! [X0,X1,X2] :
( ( 'point$uequal'(X1,X2)
& 'point$uequal'(X0,X1) )
=> 'point$uequal'(X0,X2) ) ).
fof(reflexivity_of_line_equal,axiom,
! [X0,X1] :
( incident(X0,X1)
=> 'line$uequal'(X1,X1) ) ).
fof(symmetry_of_line_equal,axiom,
! [X0,X1] :
( 'line$uequal'(X0,X1)
=> 'line$uequal'(X1,X0) ) ).
fof(transitivity_of_line_equal,axiom,
! [X0,X1,X2] :
( ( 'line$uequal'(X1,X2)
& 'line$uequal'(X0,X1) )
=> 'line$uequal'(X0,X2) ) ).
fof(pcon,axiom,
! [X0,X1,X2] :
( ( incident(X1,X2)
& 'point$uequal'(X0,X1) )
=> incident(X0,X2) ) ).
fof(lcon,axiom,
! [X0,X1,X2] :
( ( 'line$uequal'(X1,X2)
& incident(X0,X1) )
=> incident(X0,X2) ) ).
fof(unique,axiom,
! [X0,X1,X2,X3] :
( ( incident(X1,X3)
& incident(X1,X2)
& incident(X0,X3)
& incident(X0,X2) )
=> ( 'line$uequal'(X2,X3)
| 'point$uequal'(X0,X1) ) ) ).
fof(goal_to_be_proved,conjecture,
goal ).
fof(negated_conjecture,negated_conjecture,
~ goal,
inference(negate_conjecture,[status(cth)],[goal_to_be_proved]) ).
cnf(c0,plain,
( goal
| ~ incident(ab,X0)
| ~ incident(ac,X0)
| ~ incident(bc,X0)
| ~ 'line$uequal'(X0,X0) ),
inference(clausification,[status(esa)],[goal_normal]) ).
cnf(c1,plain,
( goal
| ~ incident(c1,a2b2)
| ~ incident(b1,a2c2)
| ~ incident(a1,b2c2) ),
inference(clausification,[status(esa)],[t1in2]) ).
cnf(c2,plain,
( goal
| ~ incident(c2,a1b1)
| ~ incident(b2,a1c1)
| ~ incident(a2,b1c1) ),
inference(clausification,[status(esa)],[t2in1]) ).
cnf(c3,plain,
( incident(b2,a1c1)
| incident(a1,b2c2) ),
inference(clausification,[status(esa)],[gap_a]) ).
cnf(c4,plain,
( incident(c2,a1b1)
| incident(b1,a2c2) ),
inference(clausification,[status(esa)],[gap_b]) ).
cnf(c5,plain,
( incident(a2,b1c1)
| incident(c1,a2b2) ),
inference(clausification,[status(esa)],[gap_c]) ).
cnf(c6,plain,
incident(a1,a1b1),
inference(clausification,[status(esa)],[ia1b1]) ).
cnf(c7,plain,
incident(b1,a1b1),
inference(clausification,[status(esa)],[ib1a1]) ).
cnf(c8,plain,
incident(a2,a2b2),
inference(clausification,[status(esa)],[ia2b2]) ).
cnf(c9,plain,
incident(b2,a2b2),
inference(clausification,[status(esa)],[ib2a2]) ).
cnf(c10,plain,
incident(a1,a1c1),
inference(clausification,[status(esa)],[ia1c1]) ).
cnf(c11,plain,
incident(c1,a1c1),
inference(clausification,[status(esa)],[ic1a1]) ).
cnf(c12,plain,
incident(a2,a2c2),
inference(clausification,[status(esa)],[ia2c2]) ).
cnf(c13,plain,
incident(c2,a2c2),
inference(clausification,[status(esa)],[ic2a2]) ).
cnf(c14,plain,
incident(c1,b1c1),
inference(clausification,[status(esa)],[ic1b1]) ).
cnf(c15,plain,
incident(b1,b1c1),
inference(clausification,[status(esa)],[ib1c1]) ).
cnf(c16,plain,
incident(c2,b2c2),
inference(clausification,[status(esa)],[ic2b2]) ).
cnf(c17,plain,
incident(b2,b2c2),
inference(clausification,[status(esa)],[ib2c2]) ).
cnf(c18,plain,
incident(o,oa),
inference(clausification,[status(esa)],[iooa]) ).
cnf(c19,plain,
incident(o,ob),
inference(clausification,[status(esa)],[ioob]) ).
cnf(c20,plain,
incident(o,oc),
inference(clausification,[status(esa)],[iooc]) ).
cnf(c21,plain,
incident(a1,oa),
inference(clausification,[status(esa)],[ia1oa]) ).
cnf(c22,plain,
incident(a2,oa),
inference(clausification,[status(esa)],[ia2oa]) ).
cnf(c23,plain,
incident(b1,ob),
inference(clausification,[status(esa)],[ib1ob]) ).
cnf(c24,plain,
incident(b2,ob),
inference(clausification,[status(esa)],[ib2ob]) ).
cnf(c25,plain,
incident(c1,oc),
inference(clausification,[status(esa)],[ic1oc]) ).
cnf(c26,plain,
incident(c2,oc),
inference(clausification,[status(esa)],[ic2oc]) ).
cnf(c27,plain,
incident(bc,b1c1),
inference(clausification,[status(esa)],[ibc1]) ).
cnf(c28,plain,
incident(bc,b2c2),
inference(clausification,[status(esa)],[ibc2]) ).
cnf(c29,plain,
incident(ac,a1c1),
inference(clausification,[status(esa)],[iac1]) ).
cnf(c30,plain,
incident(ac,a2c2),
inference(clausification,[status(esa)],[iac2]) ).
cnf(c31,plain,
incident(ab,a1b1),
inference(clausification,[status(esa)],[iab1]) ).
cnf(c32,plain,
incident(ab,a2b2),
inference(clausification,[status(esa)],[iab2]) ).
cnf(c33,plain,
( goal
| ~ incident(c1,X0)
| ~ incident(b1,X0)
| ~ incident(a1,X0) ),
inference(clausification,[status(esa)],[triangle1]) ).
cnf(c34,plain,
( goal
| ~ incident(c2,X0)
| ~ incident(b2,X0)
| ~ incident(a2,X0) ),
inference(clausification,[status(esa)],[triangle2]) ).
cnf(c35,plain,
( goal
| ~ 'point$uequal'(a2,a1) ),
inference(clausification,[status(esa)],[notaa]) ).
cnf(c36,plain,
( goal
| ~ 'point$uequal'(b2,b1) ),
inference(clausification,[status(esa)],[notbb]) ).
cnf(c37,plain,
( goal
| ~ 'point$uequal'(c2,c1) ),
inference(clausification,[status(esa)],[notcc]) ).
cnf(c38,plain,
( goal
| ~ 'line$uequal'(b1c1,b2c2) ),
inference(clausification,[status(esa)],[notbc]) ).
cnf(c39,plain,
( goal
| ~ 'line$uequal'(a1c1,a2c2) ),
inference(clausification,[status(esa)],[notac]) ).
cnf(c40,plain,
( goal
| ~ 'line$uequal'(a1b1,a2b2) ),
inference(clausification,[status(esa)],[notab]) ).
cnf(c42,plain,
( 'point$uequal'(X1,X0)
| ~ 'point$uequal'(X0,X1) ),
inference(clausification,[status(esa)],[symmetry_of_point_equal]) ).
cnf(c43,plain,
( 'point$uequal'(X0,X2)
| ~ 'point$uequal'(X1,X2)
| ~ 'point$uequal'(X0,X1) ),
inference(clausification,[status(esa)],[transitivity_of_point_equal]) ).
cnf(c44,plain,
( 'line$uequal'(X1,X1)
| ~ incident(X0,X1) ),
inference(clausification,[status(esa)],[reflexivity_of_line_equal]) ).
cnf(c45,plain,
( 'line$uequal'(X1,X0)
| ~ 'line$uequal'(X0,X1) ),
inference(clausification,[status(esa)],[symmetry_of_line_equal]) ).
cnf(c46,plain,
( 'line$uequal'(X0,X2)
| ~ 'line$uequal'(X1,X2)
| ~ 'line$uequal'(X0,X1) ),
inference(clausification,[status(esa)],[transitivity_of_line_equal]) ).
cnf(c47,plain,
( incident(X0,X2)
| ~ incident(X1,X2)
| ~ 'point$uequal'(X0,X1) ),
inference(clausification,[status(esa)],[pcon]) ).
cnf(c48,plain,
( incident(X0,X2)
| ~ 'line$uequal'(X1,X2)
| ~ incident(X0,X1) ),
inference(clausification,[status(esa)],[lcon]) ).
cnf(c49,plain,
( 'line$uequal'(X1,X3)
| 'point$uequal'(X0,X2)
| ~ incident(X2,X1)
| ~ incident(X0,X3)
| ~ incident(X2,X3)
| ~ incident(X0,X1) ),
inference(clausification,[status(esa)],[unique]) ).
cnf(c50,plain,
~ goal,
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(d0,plain,
( 'point$uequal'(ab,X0)
| 'line$uequal'(a1b1,X1)
| ~ incident(ab,X1)
| ~ incident(X0,a1b1)
| ~ incident(X0,X1) ),
inference(resolution,[status(thm)],[c49,c31]) ).
cnf(d1,plain,
( 'point$uequal'(ab,X0)
| 'line$uequal'(a1b1,a2b2)
| ~ incident(X0,a1b1)
| ~ incident(X0,a2b2) ),
inference(resolution,[status(thm)],[d0,c32]) ).
cnf(d2,plain,
~ 'line$uequal'(a1b1,a2b2),
inference(resolution,[status(thm)],[c50,c40]) ).
cnf(d3,plain,
( 'point$uequal'(ab,X0)
| ~ incident(X0,a1b1)
| ~ incident(X0,a2b2) ),
inference(resolution,[status(thm)],[d2,d1]) ).
cnf(d4,plain,
( 'point$uequal'(ab,a1)
| ~ incident(a1,a2b2) ),
inference(resolution,[status(thm)],[d3,c6]) ).
cnf(d5,plain,
( 'point$uequal'(c2,X0)
| 'line$uequal'(oc,X1)
| ~ incident(c2,X1)
| ~ incident(X0,oc)
| ~ incident(X0,X1) ),
inference(resolution,[status(thm)],[c49,c26]) ).
cnf(d6,plain,
( 'point$uequal'(c2,X0)
| 'line$uequal'(oc,b2c2)
| ~ incident(X0,oc)
| ~ incident(X0,b2c2) ),
inference(resolution,[status(thm)],[d5,c16]) ).
cnf(d7,plain,
( 'point$uequal'(c2,c1)
| 'line$uequal'(oc,b2c2)
| ~ incident(c1,b2c2) ),
inference(resolution,[status(thm)],[d6,c25]) ).
cnf(d8,plain,
~ 'point$uequal'(c2,c1),
inference(resolution,[status(thm)],[c50,c37]) ).
cnf(d9,plain,
( 'line$uequal'(oc,b2c2)
| ~ incident(c1,b2c2) ),
inference(resolution,[status(thm)],[d8,d7]) ).
cnf(d10,plain,
( ~ 'line$uequal'(X0,X0)
| ~ incident(ab,X0)
| ~ incident(ac,X0)
| ~ incident(bc,X0) ),
inference(resolution,[status(thm)],[c50,c0]) ).
cnf(d11,plain,
'line$uequal'(a2b2,a2b2),
inference(resolution,[status(thm)],[c44,c32]) ).
cnf(d12,plain,
( ~ incident(ab,a2b2)
| ~ incident(ac,a2b2)
| ~ incident(bc,a2b2) ),
inference(resolution,[status(thm)],[d11,d10]) ).
cnf(d13,plain,
( ~ incident(ac,a2b2)
| ~ incident(bc,a2b2) ),
inference(resolution,[status(thm)],[c32,d12]) ).
cnf(d14,plain,
( 'point$uequal'(b2,X0)
| 'line$uequal'(a2b2,X1)
| ~ incident(b2,X1)
| ~ incident(X0,a2b2)
| ~ incident(X0,X1) ),
inference(resolution,[status(thm)],[c49,c9]) ).
cnf(d15,plain,
( incident(a1,b2c2)
| 'point$uequal'(b2,X0)
| 'line$uequal'(a2b2,a1c1)
| ~ incident(X0,a2b2)
| ~ incident(X0,a1c1) ),
inference(resolution,[status(thm)],[d14,c3]) ).
cnf(d16,plain,
( 'point$uequal'(b2,c1)
| 'line$uequal'(a2b2,a1c1)
| incident(a1,b2c2)
| ~ incident(c1,a2b2) ),
inference(resolution,[status(thm)],[d15,c11]) ).
cnf(d17,plain,
( ~ incident(a1,X0)
| ~ incident(c1,X0)
| ~ incident(b1,X0) ),
inference(resolution,[status(thm)],[c50,c33]) ).
cnf(d18,plain,
( 'point$uequal'(c1,X0)
| 'line$uequal'(oc,X1)
| ~ incident(c1,X1)
| ~ incident(X0,oc)
| ~ incident(X0,X1) ),
inference(resolution,[status(thm)],[c49,c25]) ).
cnf(d19,plain,
( 'point$uequal'(c1,X0)
| 'line$uequal'(oc,b1c1)
| ~ incident(X0,oc)
| ~ incident(X0,b1c1) ),
inference(resolution,[status(thm)],[d18,c14]) ).
cnf(d20,plain,
( 'point$uequal'(c1,c2)
| 'line$uequal'(oc,b1c1)
| ~ incident(c2,b1c1) ),
inference(resolution,[status(thm)],[d19,c26]) ).
cnf(d21,plain,
'line$uequal'(oc,oc),
inference(resolution,[status(thm)],[c44,c26]) ).
cnf(d22,plain,
( ~ incident(ab,oc)
| ~ incident(ac,oc)
| ~ incident(bc,oc) ),
inference(resolution,[status(thm)],[d21,d10]) ).
cnf(d23,plain,
( 'point$uequal'(a1,X0)
| 'line$uequal'(oa,X1)
| ~ incident(a1,X1)
| ~ incident(X0,oa)
| ~ incident(X0,X1) ),
inference(resolution,[status(thm)],[c49,c21]) ).
cnf(d24,plain,
( 'point$uequal'(a1,X0)
| 'line$uequal'(oa,a1b1)
| ~ incident(X0,oa)
| ~ incident(X0,a1b1) ),
inference(resolution,[status(thm)],[d23,c6]) ).
cnf(d25,plain,
( 'point$uequal'(a1,a2)
| 'line$uequal'(oa,a1b1)
| ~ incident(a2,a1b1) ),
inference(resolution,[status(thm)],[d24,c22]) ).
cnf(d26,plain,
( 'point$uequal'(a2,X0)
| 'line$uequal'(a2c2,X1)
| ~ incident(a2,X1)
| ~ incident(X0,a2c2)
| ~ incident(X0,X1) ),
inference(resolution,[status(thm)],[c49,c12]) ).
cnf(d27,plain,
( incident(c1,a2b2)
| 'point$uequal'(a2,X0)
| 'line$uequal'(a2c2,b1c1)
| ~ incident(X0,a2c2)
| ~ incident(X0,b1c1) ),
inference(resolution,[status(thm)],[d26,c5]) ).
cnf(d28,plain,
( 'point$uequal'(a2,b1)
| 'line$uequal'(a2c2,b1c1)
| incident(c1,a2b2)
| ~ incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d27,c15]) ).
cnf(d29,plain,
( 'point$uequal'(ac,X0)
| 'line$uequal'(a1c1,X1)
| ~ incident(ac,X1)
| ~ incident(X0,a1c1)
| ~ incident(X0,X1) ),
inference(resolution,[status(thm)],[c49,c29]) ).
cnf(d30,plain,
( 'point$uequal'(ac,X0)
| 'line$uequal'(a1c1,a2c2)
| ~ incident(X0,a1c1)
| ~ incident(X0,a2c2) ),
inference(resolution,[status(thm)],[d29,c30]) ).
cnf(d31,plain,
~ 'line$uequal'(a1c1,a2c2),
inference(resolution,[status(thm)],[c50,c39]) ).
cnf(d32,plain,
( 'point$uequal'(ac,X0)
| ~ incident(X0,a1c1)
| ~ incident(X0,a2c2) ),
inference(resolution,[status(thm)],[d31,d30]) ).
cnf(d33,plain,
( 'point$uequal'(bc,X0)
| 'line$uequal'(b1c1,X1)
| ~ incident(bc,X1)
| ~ incident(X0,b1c1)
| ~ incident(X0,X1) ),
inference(resolution,[status(thm)],[c49,c27]) ).
cnf(d34,plain,
( 'point$uequal'(bc,X0)
| 'line$uequal'(b1c1,b2c2)
| ~ incident(X0,b1c1)
| ~ incident(X0,b2c2) ),
inference(resolution,[status(thm)],[d33,c28]) ).
cnf(d35,plain,
~ 'line$uequal'(b1c1,b2c2),
inference(resolution,[status(thm)],[c50,c38]) ).
cnf(d36,plain,
( 'point$uequal'(bc,X0)
| ~ incident(X0,b1c1)
| ~ incident(X0,b2c2) ),
inference(resolution,[status(thm)],[d35,d34]) ).
cnf(d37,plain,
( 'point$uequal'(b1,X0)
| 'line$uequal'(ob,X1)
| ~ incident(b1,X1)
| ~ incident(X0,ob)
| ~ incident(X0,X1) ),
inference(resolution,[status(thm)],[c49,c23]) ).
cnf(d38,plain,
( 'point$uequal'(b1,X0)
| 'line$uequal'(ob,b1c1)
| ~ incident(X0,ob)
| ~ incident(X0,b1c1) ),
inference(resolution,[status(thm)],[d37,c15]) ).
cnf(d39,plain,
( 'point$uequal'(b1,b2)
| 'line$uequal'(ob,b1c1)
| ~ incident(b2,b1c1) ),
inference(resolution,[status(thm)],[d38,c24]) ).
cnf(d40,plain,
( incident(a1,b2c2)
| 'point$uequal'(b2,X0)
| 'line$uequal'(a1c1,X1)
| ~ incident(b2,X1)
| ~ incident(X0,a1c1)
| ~ incident(X0,X1) ),
inference(resolution,[status(thm)],[c49,c3]) ).
cnf(d41,plain,
( 'point$uequal'(b2,X0)
| 'line$uequal'(a1c1,a2b2)
| incident(a1,b2c2)
| ~ incident(X0,a1c1)
| ~ incident(X0,a2b2) ),
inference(resolution,[status(thm)],[d40,c9]) ).
cnf(d42,plain,
( 'point$uequal'(b2,c1)
| 'line$uequal'(a1c1,a2b2)
| incident(a1,b2c2)
| ~ incident(c1,a2b2) ),
inference(resolution,[status(thm)],[d41,c11]) ).
cnf(d43,plain,
( ~ incident(b2,a1c1)
| ~ incident(a2,b1c1)
| ~ incident(c2,a1b1) ),
inference(resolution,[status(thm)],[c50,c2]) ).
cnf(d44,plain,
( ~ incident(a2,b1c1)
| ~ incident(c2,a1b1)
| incident(a1,b2c2) ),
inference(resolution,[status(thm)],[c3,d43]) ).
cnf(d45,plain,
( ~ incident(c2,a1b1)
| incident(a1,b2c2)
| incident(c1,a2b2) ),
inference(resolution,[status(thm)],[c5,d44]) ).
cnf(d46,plain,
( incident(b1,a2c2)
| incident(a1,b2c2)
| incident(c1,a2b2) ),
inference(resolution,[status(thm)],[d45,c4]) ).
cnf(d47,plain,
( 'point$uequal'(ac,a1)
| ~ incident(a1,a2c2) ),
inference(resolution,[status(thm)],[d32,c10]) ).
cnf(d48,plain,
( 'point$uequal'(a2,X0)
| 'line$uequal'(a2c2,oa)
| ~ incident(X0,a2c2)
| ~ incident(X0,oa) ),
inference(resolution,[status(thm)],[d26,c22]) ).
cnf(d49,plain,
( incident(b1,a2c2)
| 'point$uequal'(c2,X0)
| 'line$uequal'(oc,a1b1)
| ~ incident(X0,oc)
| ~ incident(X0,a1b1) ),
inference(resolution,[status(thm)],[d5,c4]) ).
cnf(d50,plain,
( 'point$uequal'(c2,o)
| 'line$uequal'(oc,a1b1)
| incident(b1,a2c2)
| ~ incident(o,a1b1) ),
inference(resolution,[status(thm)],[d49,c20]) ).
cnf(d51,plain,
( incident(c1,a2b2)
| incident(b1,a2c2)
| 'point$uequal'(a1,X0)
| 'line$uequal'(b2c2,X1)
| ~ incident(a1,X1)
| ~ incident(X0,b2c2)
| ~ incident(X0,X1) ),
inference(resolution,[status(thm)],[c49,d46]) ).
cnf(d52,plain,
( 'point$uequal'(a1,X0)
| 'line$uequal'(b2c2,a1b1)
| incident(c1,a2b2)
| incident(b1,a2c2)
| ~ incident(X0,b2c2)
| ~ incident(X0,a1b1) ),
inference(resolution,[status(thm)],[d51,c6]) ).
cnf(d53,plain,
( incident(b1,a2c2)
| 'point$uequal'(a1,c2)
| 'line$uequal'(b2c2,a1b1)
| incident(c1,a2b2)
| incident(b1,a2c2)
| ~ incident(c2,b2c2) ),
inference(resolution,[status(thm)],[d52,c4]) ).
cnf(d54,plain,
( 'point$uequal'(a1,c2)
| 'line$uequal'(b2c2,a1b1)
| incident(c1,a2b2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[c16,d53]) ).
cnf(d55,plain,
( 'point$uequal'(c2,a1)
| 'line$uequal'(b2c2,a1b1)
| incident(c1,a2b2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d54,c42]) ).
cnf(d56,plain,
( ~ incident(a1,X0)
| incident(c2,X0)
| 'line$uequal'(b2c2,a1b1)
| incident(c1,a2b2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d55,c47]) ).
cnf(d57,plain,
( 'line$uequal'(b2c2,a1b1)
| incident(c2,oa)
| incident(c1,a2b2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d56,c21]) ).
cnf(d58,plain,
( ~ incident(X0,b2c2)
| incident(X0,a1b1)
| incident(c2,oa)
| incident(c1,a2b2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d57,c48]) ).
cnf(d59,plain,
( incident(c2,oa)
| incident(c1,a2b2)
| incident(b1,a2c2)
| incident(b2,a1b1) ),
inference(resolution,[status(thm)],[d58,c17]) ).
cnf(d60,plain,
( 'point$uequal'(b1,X0)
| 'line$uequal'(a1b1,X1)
| ~ incident(b1,X1)
| ~ incident(X0,a1b1)
| ~ incident(X0,X1) ),
inference(resolution,[status(thm)],[c49,c7]) ).
cnf(d61,plain,
( 'point$uequal'(b1,X0)
| 'line$uequal'(a1b1,ob)
| ~ incident(X0,a1b1)
| ~ incident(X0,ob) ),
inference(resolution,[status(thm)],[d60,c23]) ).
cnf(d62,plain,
( 'point$uequal'(b1,b2)
| 'line$uequal'(a1b1,ob)
| ~ incident(b2,a1b1) ),
inference(resolution,[status(thm)],[d61,c24]) ).
cnf(d63,plain,
( incident(c2,oa)
| incident(c1,a2b2)
| incident(b1,a2c2)
| 'point$uequal'(b1,b2)
| 'line$uequal'(a1b1,ob) ),
inference(resolution,[status(thm)],[d62,d59]) ).
cnf(d64,plain,
( 'point$uequal'(b2,b1)
| 'line$uequal'(a1b1,ob)
| incident(c2,oa)
| incident(c1,a2b2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d63,c42]) ).
cnf(d65,plain,
~ 'point$uequal'(b2,b1),
inference(resolution,[status(thm)],[c50,c36]) ).
cnf(d66,plain,
( 'line$uequal'(a1b1,ob)
| incident(c2,oa)
| incident(c1,a2b2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d65,d64]) ).
cnf(d67,plain,
( 'line$uequal'(ob,a1b1)
| incident(c2,oa)
| incident(c1,a2b2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d66,c45]) ).
cnf(d68,plain,
( ~ incident(X0,ob)
| incident(X0,a1b1)
| incident(c2,oa)
| incident(c1,a2b2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d67,c48]) ).
cnf(d69,plain,
( incident(c2,oa)
| incident(c1,a2b2)
| incident(b1,a2c2)
| incident(o,a1b1) ),
inference(resolution,[status(thm)],[d68,c19]) ).
cnf(d70,plain,
( 'point$uequal'(c2,o)
| 'line$uequal'(oc,a1b1)
| incident(b1,a2c2)
| incident(c2,oa)
| incident(c1,a2b2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d69,d50]) ).
cnf(d71,plain,
( ~ incident(o,X0)
| incident(c2,X0)
| 'line$uequal'(oc,a1b1)
| incident(c2,oa)
| incident(c1,a2b2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d70,c47]) ).
cnf(d72,plain,
( 'line$uequal'(oc,a1b1)
| incident(c2,oa)
| incident(c2,oa)
| incident(c1,a2b2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d71,c18]) ).
cnf(d73,plain,
( ~ incident(X0,oc)
| incident(X0,a1b1)
| incident(c2,oa)
| incident(c1,a2b2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d72,c48]) ).
cnf(d74,plain,
( incident(c2,oa)
| incident(c1,a2b2)
| incident(b1,a2c2)
| incident(c1,a1b1) ),
inference(resolution,[status(thm)],[d73,c25]) ).
cnf(d75,plain,
( ~ incident(c1,a1b1)
| ~ incident(b1,a1b1) ),
inference(resolution,[status(thm)],[d17,c6]) ).
cnf(d76,plain,
~ incident(c1,a1b1),
inference(resolution,[status(thm)],[c7,d75]) ).
cnf(d77,plain,
( incident(c2,oa)
| incident(c1,a2b2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d76,d74]) ).
cnf(d78,plain,
( 'point$uequal'(a2,c2)
| 'line$uequal'(a2c2,oa)
| ~ incident(c2,a2c2)
| incident(c1,a2b2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d77,d48]) ).
cnf(d79,plain,
( 'point$uequal'(a2,c2)
| 'line$uequal'(a2c2,oa)
| incident(c1,a2b2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[c13,d78]) ).
cnf(d80,plain,
( ~ incident(c2,X0)
| incident(a2,X0)
| 'line$uequal'(a2c2,oa)
| incident(c1,a2b2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d79,c47]) ).
cnf(d81,plain,
( 'line$uequal'(a2c2,oa)
| incident(a2,b2c2)
| incident(c1,a2b2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d80,c16]) ).
cnf(d82,plain,
( ~ incident(b2,X0)
| ~ incident(a2,X0)
| ~ incident(c2,X0) ),
inference(resolution,[status(thm)],[c50,c34]) ).
cnf(d83,plain,
( ~ incident(a2,b2c2)
| ~ incident(c2,b2c2) ),
inference(resolution,[status(thm)],[d82,c17]) ).
cnf(d84,plain,
~ incident(a2,b2c2),
inference(resolution,[status(thm)],[c16,d83]) ).
cnf(d85,plain,
( 'line$uequal'(a2c2,oa)
| incident(c1,a2b2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d84,d81]) ).
cnf(d86,plain,
( 'line$uequal'(oa,a2c2)
| incident(c1,a2b2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d85,c45]) ).
cnf(d87,plain,
( ~ incident(X0,oa)
| incident(X0,a2c2)
| incident(c1,a2b2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d86,c48]) ).
cnf(d88,plain,
( incident(c1,a2b2)
| incident(b1,a2c2)
| incident(a1,a2c2) ),
inference(resolution,[status(thm)],[d87,c21]) ).
cnf(d89,plain,
( 'point$uequal'(ac,a1)
| incident(c1,a2b2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d88,d47]) ).
cnf(d90,plain,
( ~ incident(a1,X0)
| incident(ac,X0)
| incident(c1,a2b2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d89,c47]) ).
cnf(d91,plain,
( incident(c1,a2b2)
| incident(b1,a2c2)
| incident(c1,a2b2)
| incident(b1,a2c2)
| incident(ac,b2c2) ),
inference(resolution,[status(thm)],[d90,d46]) ).
cnf(d92,plain,
'line$uequal'(b2c2,b2c2),
inference(resolution,[status(thm)],[c44,c28]) ).
cnf(d93,plain,
( ~ incident(ab,b2c2)
| ~ incident(ac,b2c2)
| ~ incident(bc,b2c2) ),
inference(resolution,[status(thm)],[d92,d10]) ).
cnf(d94,plain,
( ~ incident(ab,b2c2)
| ~ incident(ac,b2c2) ),
inference(resolution,[status(thm)],[c28,d93]) ).
cnf(d95,plain,
( incident(c1,a2b2)
| incident(b1,a2c2)
| incident(o,a2c2) ),
inference(resolution,[status(thm)],[d87,c18]) ).
cnf(d96,plain,
( 'point$uequal'(b1,o)
| 'line$uequal'(a1b1,ob)
| ~ incident(o,a1b1) ),
inference(resolution,[status(thm)],[d61,c19]) ).
cnf(d97,plain,
( 'point$uequal'(o,X0)
| 'line$uequal'(oa,X1)
| ~ incident(o,X1)
| ~ incident(X0,oa)
| ~ incident(X0,X1) ),
inference(resolution,[status(thm)],[c49,c18]) ).
cnf(d98,plain,
( 'point$uequal'(o,X0)
| 'line$uequal'(oa,oc)
| ~ incident(X0,oa)
| ~ incident(X0,oc) ),
inference(resolution,[status(thm)],[d97,c20]) ).
cnf(d99,plain,
( 'point$uequal'(o,c2)
| 'line$uequal'(oa,oc)
| ~ incident(c2,oa) ),
inference(resolution,[status(thm)],[d98,c26]) ).
cnf(d100,plain,
( 'point$uequal'(o,c2)
| 'line$uequal'(oa,oc)
| incident(c1,a2b2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d77,d99]) ).
cnf(d101,plain,
( ~ incident(c2,X0)
| incident(o,X0)
| 'line$uequal'(oa,oc)
| incident(c1,a2b2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d100,c47]) ).
cnf(d102,plain,
( incident(b1,a2c2)
| 'line$uequal'(oa,oc)
| incident(o,a1b1)
| incident(c1,a2b2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d101,c4]) ).
cnf(d103,plain,
( 'line$uequal'(a2c2,X0)
| ~ 'line$uequal'(oa,X0)
| incident(c1,a2b2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d85,c46]) ).
cnf(d104,plain,
( incident(o,a1b1)
| incident(c1,a2b2)
| incident(b1,a2c2)
| 'line$uequal'(a2c2,oc)
| incident(c1,a2b2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d103,d102]) ).
cnf(d105,plain,
( 'line$uequal'(oc,a2c2)
| incident(o,a1b1)
| incident(c1,a2b2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d104,c45]) ).
cnf(d106,plain,
( 'point$uequal'(c1,X0)
| 'line$uequal'(a1c1,X1)
| ~ incident(c1,X1)
| ~ incident(X0,a1c1)
| ~ incident(X0,X1) ),
inference(resolution,[status(thm)],[c49,c11]) ).
cnf(d107,plain,
( 'point$uequal'(c1,X0)
| 'line$uequal'(a1c1,oc)
| ~ incident(X0,a1c1)
| ~ incident(X0,oc) ),
inference(resolution,[status(thm)],[d106,c25]) ).
cnf(d108,plain,
( 'point$uequal'(c1,c2)
| 'line$uequal'(a1c1,oc)
| ~ incident(c2,a1c1) ),
inference(resolution,[status(thm)],[d107,c26]) ).
cnf(d109,plain,
( 'line$uequal'(b2c2,a1b1)
| incident(c2,a1c1)
| incident(c1,a2b2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d56,c10]) ).
cnf(d110,plain,
( 'line$uequal'(a1b1,b2c2)
| incident(c2,a1c1)
| incident(c1,a2b2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d109,c45]) ).
cnf(d111,plain,
( ~ incident(X0,a1b1)
| incident(X0,b2c2)
| incident(c2,a1c1)
| incident(c1,a2b2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d110,c48]) ).
cnf(d112,plain,
( incident(c2,a1c1)
| incident(c1,a2b2)
| incident(b1,a2c2)
| incident(ab,b2c2) ),
inference(resolution,[status(thm)],[d111,c31]) ).
cnf(d113,plain,
( ~ incident(ac,b2c2)
| incident(c2,a1c1)
| incident(c1,a2b2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d112,d94]) ).
cnf(d114,plain,
( incident(c2,a1c1)
| incident(c1,a2b2)
| incident(b1,a2c2)
| incident(c1,a2b2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d91,d113]) ).
cnf(d115,plain,
( 'point$uequal'(c1,c2)
| 'line$uequal'(a1c1,oc)
| incident(c1,a2b2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d114,d108]) ).
cnf(d116,plain,
( 'point$uequal'(c2,c1)
| 'line$uequal'(a1c1,oc)
| incident(c1,a2b2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d115,c42]) ).
cnf(d117,plain,
( 'line$uequal'(a1c1,oc)
| incident(c1,a2b2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d8,d116]) ).
cnf(d118,plain,
( 'line$uequal'(a1c1,X0)
| ~ 'line$uequal'(oc,X0)
| incident(c1,a2b2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d117,c46]) ).
cnf(d119,plain,
( incident(o,a1b1)
| incident(c1,a2b2)
| incident(b1,a2c2)
| 'line$uequal'(a1c1,a2c2)
| incident(c1,a2b2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d118,d105]) ).
cnf(d120,plain,
( incident(o,a1b1)
| incident(c1,a2b2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d31,d119]) ).
cnf(d121,plain,
( 'point$uequal'(b1,o)
| 'line$uequal'(a1b1,ob)
| incident(c1,a2b2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d120,d96]) ).
cnf(d122,plain,
( ~ incident(o,X0)
| incident(b1,X0)
| 'line$uequal'(a1b1,ob)
| incident(c1,a2b2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d121,c47]) ).
cnf(d123,plain,
( incident(c1,a2b2)
| incident(b1,a2c2)
| 'line$uequal'(a1b1,ob)
| incident(c1,a2b2)
| incident(b1,a2c2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d122,d95]) ).
cnf(d124,plain,
( 'line$uequal'(ob,a1b1)
| incident(c1,a2b2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d123,c45]) ).
cnf(d125,plain,
( ~ incident(X0,ob)
| incident(X0,a1b1)
| incident(c1,a2b2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d124,c48]) ).
cnf(d126,plain,
( incident(c1,a2b2)
| incident(b1,a2c2)
| incident(b2,a1b1) ),
inference(resolution,[status(thm)],[d125,c24]) ).
cnf(d127,plain,
( 'point$uequal'(ab,b2)
| ~ incident(b2,a2b2)
| incident(c1,a2b2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d126,d3]) ).
cnf(d128,plain,
( 'point$uequal'(ab,b2)
| incident(c1,a2b2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[c9,d127]) ).
cnf(d129,plain,
( ~ incident(b2,X0)
| incident(ab,X0)
| incident(c1,a2b2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d128,c47]) ).
cnf(d130,plain,
( incident(c1,a2b2)
| incident(b1,a2c2)
| incident(ab,b2c2) ),
inference(resolution,[status(thm)],[d129,c17]) ).
cnf(d131,plain,
( ~ incident(ac,b2c2)
| incident(c1,a2b2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d130,d94]) ).
cnf(d132,plain,
( incident(c1,a2b2)
| incident(b1,a2c2)
| incident(c1,a2b2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d131,d91]) ).
cnf(d133,plain,
( 'point$uequal'(b2,c1)
| 'line$uequal'(a1c1,a2b2)
| incident(a1,b2c2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d132,d42]) ).
cnf(d134,plain,
( ~ incident(c1,X0)
| incident(b2,X0)
| 'line$uequal'(a1c1,a2b2)
| incident(a1,b2c2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d133,c47]) ).
cnf(d135,plain,
( 'line$uequal'(a1c1,a2b2)
| incident(b2,b1c1)
| incident(a1,b2c2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d134,c14]) ).
cnf(d136,plain,
( 'line$uequal'(a2b2,a1c1)
| incident(b2,b1c1)
| incident(a1,b2c2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d135,c45]) ).
cnf(d137,plain,
( ~ incident(X0,a2b2)
| incident(X0,a1c1)
| incident(b2,b1c1)
| incident(a1,b2c2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d136,c48]) ).
cnf(d138,plain,
( incident(b2,b1c1)
| incident(a1,b2c2)
| incident(b1,a2c2)
| incident(a2,a1c1) ),
inference(resolution,[status(thm)],[d137,c8]) ).
cnf(d139,plain,
( 'point$uequal'(b1,b2)
| 'line$uequal'(ob,b1c1)
| incident(a2,a1c1)
| incident(a1,b2c2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d138,d39]) ).
cnf(d140,plain,
( 'point$uequal'(b2,b1)
| 'line$uequal'(ob,b1c1)
| incident(a2,a1c1)
| incident(a1,b2c2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d139,c42]) ).
cnf(d141,plain,
( 'line$uequal'(ob,b1c1)
| incident(a2,a1c1)
| incident(a1,b2c2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d65,d140]) ).
cnf(d142,plain,
( ~ incident(X0,ob)
| incident(X0,b1c1)
| incident(a2,a1c1)
| incident(a1,b2c2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d141,c48]) ).
cnf(d143,plain,
( incident(a2,a1c1)
| incident(a1,b2c2)
| incident(b1,a2c2)
| incident(o,b1c1) ),
inference(resolution,[status(thm)],[d142,c19]) ).
cnf(d144,plain,
( 'point$uequal'(bc,o)
| ~ incident(o,b2c2)
| incident(a2,a1c1)
| incident(a1,b2c2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d143,d36]) ).
cnf(d145,plain,
( 'point$uequal'(c2,X0)
| 'line$uequal'(b2c2,X1)
| ~ incident(c2,X1)
| ~ incident(X0,b2c2)
| ~ incident(X0,X1) ),
inference(resolution,[status(thm)],[c49,c16]) ).
cnf(d146,plain,
( 'point$uequal'(c2,X0)
| 'line$uequal'(b2c2,oc)
| ~ incident(X0,b2c2)
| ~ incident(X0,oc) ),
inference(resolution,[status(thm)],[d145,c26]) ).
cnf(d147,plain,
( 'line$uequal'(a1c1,a2b2)
| incident(b2,oc)
| incident(a1,b2c2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d134,c25]) ).
cnf(d148,plain,
( 'line$uequal'(a2b2,a1c1)
| incident(b2,oc)
| incident(a1,b2c2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d147,c45]) ).
cnf(d149,plain,
( ~ incident(X0,a2b2)
| incident(X0,a1c1)
| incident(b2,oc)
| incident(a1,b2c2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d148,c48]) ).
cnf(d150,plain,
( incident(b2,oc)
| incident(a1,b2c2)
| incident(b1,a2c2)
| incident(a2,a1c1) ),
inference(resolution,[status(thm)],[d149,c8]) ).
cnf(d151,plain,
( 'point$uequal'(c2,b2)
| 'line$uequal'(b2c2,oc)
| ~ incident(b2,b2c2)
| incident(a2,a1c1)
| incident(a1,b2c2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d150,d146]) ).
cnf(d152,plain,
( 'point$uequal'(c2,b2)
| 'line$uequal'(b2c2,oc)
| incident(a2,a1c1)
| incident(a1,b2c2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[c17,d151]) ).
cnf(d153,plain,
( ~ incident(b2,X0)
| incident(c2,X0)
| 'line$uequal'(b2c2,oc)
| incident(a2,a1c1)
| incident(a1,b2c2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d152,c47]) ).
cnf(d154,plain,
( 'line$uequal'(b2c2,oc)
| incident(a2,a1c1)
| incident(c2,a2b2)
| incident(a1,b2c2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d153,c9]) ).
cnf(d155,plain,
( ~ incident(a2,a2b2)
| ~ incident(c2,a2b2) ),
inference(resolution,[status(thm)],[d82,c9]) ).
cnf(d156,plain,
~ incident(c2,a2b2),
inference(resolution,[status(thm)],[c8,d155]) ).
cnf(d157,plain,
( 'line$uequal'(b2c2,oc)
| incident(a2,a1c1)
| incident(a1,b2c2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d156,d154]) ).
cnf(d158,plain,
( 'line$uequal'(oc,b2c2)
| incident(a2,a1c1)
| incident(a1,b2c2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d157,c45]) ).
cnf(d159,plain,
( ~ incident(X0,oc)
| incident(X0,b2c2)
| incident(a2,a1c1)
| incident(a1,b2c2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d158,c48]) ).
cnf(d160,plain,
( incident(a2,a1c1)
| incident(a1,b2c2)
| incident(b1,a2c2)
| incident(o,b2c2) ),
inference(resolution,[status(thm)],[d159,c20]) ).
cnf(d161,plain,
( 'point$uequal'(bc,o)
| incident(a2,a1c1)
| incident(a1,b2c2)
| incident(b1,a2c2)
| incident(a2,a1c1)
| incident(a1,b2c2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d160,d144]) ).
cnf(d162,plain,
( ~ incident(o,X0)
| incident(bc,X0)
| incident(a2,a1c1)
| incident(a1,b2c2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d161,c47]) ).
cnf(d163,plain,
( incident(a2,a1c1)
| incident(a1,b2c2)
| incident(b1,a2c2)
| incident(bc,oa) ),
inference(resolution,[status(thm)],[d162,c18]) ).
cnf(d164,plain,
'line$uequal'(oa,oa),
inference(resolution,[status(thm)],[c44,c22]) ).
cnf(d165,plain,
( ~ incident(ab,oa)
| ~ incident(ac,oa)
| ~ incident(bc,oa) ),
inference(resolution,[status(thm)],[d164,d10]) ).
cnf(d166,plain,
( 'point$uequal'(bc,b2)
| ~ incident(b2,b2c2)
| incident(a2,a1c1)
| incident(a1,b2c2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d138,d36]) ).
cnf(d167,plain,
( 'point$uequal'(bc,b2)
| incident(a2,a1c1)
| incident(a1,b2c2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[c17,d166]) ).
cnf(d168,plain,
( ~ incident(b2,X0)
| incident(bc,X0)
| incident(a2,a1c1)
| incident(a1,b2c2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d167,c47]) ).
cnf(d169,plain,
( incident(a1,b2c2)
| incident(a2,a1c1)
| incident(a1,b2c2)
| incident(b1,a2c2)
| incident(bc,a1c1) ),
inference(resolution,[status(thm)],[d168,c3]) ).
cnf(d170,plain,
( 'point$uequal'(o,bc)
| incident(a2,a1c1)
| incident(a1,b2c2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d161,c42]) ).
cnf(d171,plain,
( ~ incident(bc,X0)
| incident(o,X0)
| incident(a2,a1c1)
| incident(a1,b2c2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d170,c47]) ).
cnf(d172,plain,
( incident(a2,a1c1)
| incident(a1,b2c2)
| incident(b1,a2c2)
| incident(o,a1c1)
| incident(a2,a1c1)
| incident(a1,b2c2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d171,d169]) ).
cnf(d173,plain,
( 'point$uequal'(a2,X0)
| 'line$uequal'(oa,X1)
| ~ incident(a2,X1)
| ~ incident(X0,oa)
| ~ incident(X0,X1) ),
inference(resolution,[status(thm)],[c49,c22]) ).
cnf(d174,plain,
( 'point$uequal'(a2,X0)
| 'line$uequal'(oa,a2b2)
| ~ incident(X0,oa)
| ~ incident(X0,a2b2) ),
inference(resolution,[status(thm)],[d173,c8]) ).
cnf(d175,plain,
( 'point$uequal'(a2,o)
| 'line$uequal'(oa,a2b2)
| ~ incident(o,a2b2) ),
inference(resolution,[status(thm)],[d174,c18]) ).
cnf(d176,plain,
( incident(a2,a1c1)
| incident(a1,b2c2)
| incident(b1,a2c2)
| incident(bc,a2b2) ),
inference(resolution,[status(thm)],[d168,c9]) ).
cnf(d177,plain,
( incident(a2,a1c1)
| incident(a1,b2c2)
| incident(b1,a2c2)
| incident(o,a2b2)
| incident(a2,a1c1)
| incident(a1,b2c2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d171,d176]) ).
cnf(d178,plain,
( 'point$uequal'(a2,o)
| 'line$uequal'(oa,a2b2)
| incident(a2,a1c1)
| incident(a1,b2c2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d177,d175]) ).
cnf(d179,plain,
( ~ incident(o,X0)
| incident(a2,X0)
| 'line$uequal'(oa,a2b2)
| incident(a2,a1c1)
| incident(a1,b2c2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d178,c47]) ).
cnf(d180,plain,
( incident(a2,a1c1)
| incident(a1,b2c2)
| incident(b1,a2c2)
| 'line$uequal'(oa,a2b2)
| incident(a2,a1c1)
| incident(a2,a1c1)
| incident(a1,b2c2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d179,d172]) ).
cnf(d181,plain,
( 'line$uequal'(a2b2,oa)
| incident(a2,a1c1)
| incident(a1,b2c2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d180,c45]) ).
cnf(d182,plain,
( ~ incident(X0,a2b2)
| incident(X0,oa)
| incident(a2,a1c1)
| incident(a1,b2c2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d181,c48]) ).
cnf(d183,plain,
( incident(a2,a1c1)
| incident(a1,b2c2)
| incident(b1,a2c2)
| incident(ab,oa) ),
inference(resolution,[status(thm)],[d182,c32]) ).
cnf(d184,plain,
( ~ incident(ac,oa)
| ~ incident(bc,oa)
| incident(a2,a1c1)
| incident(a1,b2c2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d183,d165]) ).
cnf(d185,plain,
( 'point$uequal'(a1,X0)
| 'line$uequal'(a1c1,X1)
| ~ incident(a1,X1)
| ~ incident(X0,a1c1)
| ~ incident(X0,X1) ),
inference(resolution,[status(thm)],[c49,c10]) ).
cnf(d186,plain,
( 'point$uequal'(a1,X0)
| 'line$uequal'(a1c1,oa)
| ~ incident(X0,a1c1)
| ~ incident(X0,oa) ),
inference(resolution,[status(thm)],[d185,c21]) ).
cnf(d187,plain,
( 'point$uequal'(a1,o)
| 'line$uequal'(a1c1,oa)
| ~ incident(o,a1c1) ),
inference(resolution,[status(thm)],[d186,c18]) ).
cnf(d188,plain,
( 'point$uequal'(a1,o)
| 'line$uequal'(a1c1,oa)
| incident(a2,a1c1)
| incident(a1,b2c2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d172,d187]) ).
cnf(d189,plain,
( ~ incident(o,X0)
| incident(a1,X0)
| 'line$uequal'(a1c1,oa)
| incident(a2,a1c1)
| incident(a1,b2c2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d188,c47]) ).
cnf(d190,plain,
( incident(a2,a1c1)
| incident(a1,b2c2)
| incident(b1,a2c2)
| 'line$uequal'(a1c1,oa)
| incident(a2,a1c1)
| incident(a1,b2c2)
| incident(a1,b2c2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d189,d160]) ).
cnf(d191,plain,
( ~ incident(X0,a1c1)
| incident(X0,oa)
| incident(a2,a1c1)
| incident(a1,b2c2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d190,c48]) ).
cnf(d192,plain,
( incident(a2,a1c1)
| incident(a1,b2c2)
| incident(b1,a2c2)
| incident(ac,oa) ),
inference(resolution,[status(thm)],[d191,c29]) ).
cnf(d193,plain,
( incident(a2,a1c1)
| incident(a1,b2c2)
| incident(b1,a2c2)
| ~ incident(bc,oa)
| incident(a2,a1c1)
| incident(a1,b2c2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d192,d184]) ).
cnf(d194,plain,
( incident(a2,a1c1)
| incident(a1,b2c2)
| incident(b1,a2c2)
| incident(a2,a1c1)
| incident(a1,b2c2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d193,d163]) ).
cnf(d195,plain,
( 'point$uequal'(ac,a2)
| ~ incident(a2,a2c2)
| incident(a1,b2c2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d194,d32]) ).
cnf(d196,plain,
( 'point$uequal'(ac,a2)
| incident(a1,b2c2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[c12,d195]) ).
cnf(d197,plain,
( ~ incident(a2,X0)
| incident(ac,X0)
| incident(a1,b2c2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d196,c47]) ).
cnf(d198,plain,
( incident(a1,b2c2)
| incident(b1,a2c2)
| incident(ac,a2b2) ),
inference(resolution,[status(thm)],[d197,c8]) ).
cnf(d199,plain,
( ~ incident(bc,a2b2)
| incident(a1,b2c2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d198,d13]) ).
cnf(d200,plain,
( 'point$uequal'(a1,a2)
| 'line$uequal'(a1c1,oa)
| ~ incident(a2,a1c1) ),
inference(resolution,[status(thm)],[d186,c22]) ).
cnf(d201,plain,
( 'point$uequal'(a1,a2)
| 'line$uequal'(a1c1,oa)
| incident(a1,b2c2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d194,d200]) ).
cnf(d202,plain,
( 'point$uequal'(a2,a1)
| 'line$uequal'(a1c1,oa)
| incident(a1,b2c2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d201,c42]) ).
cnf(d203,plain,
~ 'point$uequal'(a2,a1),
inference(resolution,[status(thm)],[c50,c35]) ).
cnf(d204,plain,
( 'line$uequal'(a1c1,oa)
| incident(a1,b2c2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d203,d202]) ).
cnf(d205,plain,
( 'line$uequal'(oa,a1c1)
| incident(a1,b2c2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d204,c45]) ).
cnf(d206,plain,
( ~ incident(X0,oa)
| incident(X0,a1c1)
| incident(a1,b2c2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d205,c48]) ).
cnf(d207,plain,
( incident(a1,b2c2)
| incident(b1,a2c2)
| incident(o,a1c1) ),
inference(resolution,[status(thm)],[d206,c18]) ).
cnf(d208,plain,
( ~ 'point$uequal'(X0,ac)
| 'point$uequal'(X0,a2)
| incident(a1,b2c2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d196,c43]) ).
cnf(d209,plain,
( 'point$uequal'(b2,ac)
| 'line$uequal'(a1c1,a2b2)
| incident(a1,b2c2)
| ~ incident(ac,a2b2) ),
inference(resolution,[status(thm)],[d41,c29]) ).
cnf(d210,plain,
( 'point$uequal'(b2,ac)
| 'line$uequal'(a1c1,a2b2)
| incident(a1,b2c2)
| incident(a1,b2c2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d198,d209]) ).
cnf(d211,plain,
( 'point$uequal'(b2,a2)
| incident(a1,b2c2)
| incident(b1,a2c2)
| 'line$uequal'(a1c1,a2b2)
| incident(a1,b2c2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d210,d208]) ).
cnf(d212,plain,
( 'point$uequal'(a2,b2)
| 'line$uequal'(a1c1,a2b2)
| incident(a1,b2c2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d211,c42]) ).
cnf(d213,plain,
( ~ incident(b2,X0)
| incident(a2,X0)
| 'line$uequal'(a1c1,a2b2)
| incident(a1,b2c2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d212,c47]) ).
cnf(d214,plain,
( 'line$uequal'(a1c1,a2b2)
| incident(a2,b2c2)
| incident(a1,b2c2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d213,c17]) ).
cnf(d215,plain,
( 'line$uequal'(a1c1,a2b2)
| incident(a1,b2c2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d84,d214]) ).
cnf(d216,plain,
( ~ incident(X0,a1c1)
| incident(X0,a2b2)
| incident(a1,b2c2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d215,c48]) ).
cnf(d217,plain,
( incident(a1,b2c2)
| incident(b1,a2c2)
| incident(a1,b2c2)
| incident(b1,a2c2)
| incident(o,a2b2) ),
inference(resolution,[status(thm)],[d216,d207]) ).
cnf(d218,plain,
( 'line$uequal'(a1c1,X0)
| ~ 'line$uequal'(oa,X0)
| incident(a1,b2c2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d204,c46]) ).
cnf(d219,plain,
( 'point$uequal'(o,X0)
| 'line$uequal'(oa,ob)
| ~ incident(X0,oa)
| ~ incident(X0,ob) ),
inference(resolution,[status(thm)],[d97,c19]) ).
cnf(d220,plain,
( 'point$uequal'(o,b2)
| 'line$uequal'(oa,ob)
| ~ incident(b2,oa) ),
inference(resolution,[status(thm)],[d219,c24]) ).
cnf(d221,plain,
( ~ incident(X0,a1c1)
| incident(X0,oa)
| incident(a1,b2c2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d204,c48]) ).
cnf(d222,plain,
( incident(a1,b2c2)
| incident(a1,b2c2)
| incident(b1,a2c2)
| incident(b2,oa) ),
inference(resolution,[status(thm)],[d221,c3]) ).
cnf(d223,plain,
( 'point$uequal'(o,b2)
| 'line$uequal'(oa,ob)
| incident(a1,b2c2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d222,d220]) ).
cnf(d224,plain,
( ~ incident(b2,X0)
| incident(o,X0)
| 'line$uequal'(oa,ob)
| incident(a1,b2c2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d223,c47]) ).
cnf(d225,plain,
( 'line$uequal'(oa,ob)
| incident(o,b2c2)
| incident(a1,b2c2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d224,c17]) ).
cnf(d226,plain,
( 'line$uequal'(a1c1,ob)
| incident(a1,b2c2)
| incident(b1,a2c2)
| incident(o,b2c2)
| incident(a1,b2c2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d225,d218]) ).
cnf(d227,plain,
( 'line$uequal'(ob,a1c1)
| incident(o,b2c2)
| incident(a1,b2c2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d226,c45]) ).
cnf(d228,plain,
( ~ incident(X0,ob)
| incident(X0,a1c1)
| incident(o,b2c2)
| incident(a1,b2c2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d227,c48]) ).
cnf(d229,plain,
( incident(o,b2c2)
| incident(a1,b2c2)
| incident(b1,a2c2)
| incident(b1,a1c1) ),
inference(resolution,[status(thm)],[d228,c23]) ).
cnf(d230,plain,
( ~ incident(c1,a1c1)
| ~ incident(b1,a1c1) ),
inference(resolution,[status(thm)],[d17,c10]) ).
cnf(d231,plain,
~ incident(b1,a1c1),
inference(resolution,[status(thm)],[c11,d230]) ).
cnf(d232,plain,
( incident(o,b2c2)
| incident(a1,b2c2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d231,d229]) ).
cnf(d233,plain,
( 'point$uequal'(c1,o)
| 'line$uequal'(a1c1,oc)
| ~ incident(o,a1c1) ),
inference(resolution,[status(thm)],[d107,c20]) ).
cnf(d234,plain,
( 'point$uequal'(c1,o)
| 'line$uequal'(a1c1,oc)
| incident(a1,b2c2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d207,d233]) ).
cnf(d235,plain,
( 'point$uequal'(o,c1)
| 'line$uequal'(a1c1,oc)
| incident(a1,b2c2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d234,c42]) ).
cnf(d236,plain,
( ~ incident(c1,X0)
| incident(o,X0)
| 'line$uequal'(a1c1,oc)
| incident(a1,b2c2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d235,c47]) ).
cnf(d237,plain,
( 'line$uequal'(a1c1,oc)
| incident(o,b1c1)
| incident(a1,b2c2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d236,c14]) ).
cnf(d238,plain,
( 'line$uequal'(a2b2,a1c1)
| incident(a1,b2c2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d215,c45]) ).
cnf(d239,plain,
( 'line$uequal'(a2b2,X0)
| ~ 'line$uequal'(a1c1,X0)
| incident(a1,b2c2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d238,c46]) ).
cnf(d240,plain,
( incident(o,b1c1)
| incident(a1,b2c2)
| incident(b1,a2c2)
| 'line$uequal'(a2b2,oc)
| incident(a1,b2c2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d239,d237]) ).
cnf(d241,plain,
( 'line$uequal'(oc,a2b2)
| incident(o,b1c1)
| incident(a1,b2c2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d240,c45]) ).
cnf(d242,plain,
( ~ incident(X0,oc)
| incident(X0,a2b2)
| incident(o,b1c1)
| incident(a1,b2c2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d241,c48]) ).
cnf(d243,plain,
( incident(o,b1c1)
| incident(a1,b2c2)
| incident(b1,a2c2)
| incident(c2,a2b2) ),
inference(resolution,[status(thm)],[d242,c26]) ).
cnf(d244,plain,
( incident(o,b1c1)
| incident(a1,b2c2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d156,d243]) ).
cnf(d245,plain,
( 'point$uequal'(bc,o)
| ~ incident(o,b2c2)
| incident(a1,b2c2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d244,d36]) ).
cnf(d246,plain,
( incident(a1,b2c2)
| incident(b1,a2c2)
| 'point$uequal'(bc,o)
| incident(a1,b2c2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d245,d232]) ).
cnf(d247,plain,
( ~ incident(o,X0)
| incident(bc,X0)
| incident(a1,b2c2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d246,c47]) ).
cnf(d248,plain,
( incident(a1,b2c2)
| incident(b1,a2c2)
| incident(a1,b2c2)
| incident(b1,a2c2)
| incident(bc,a2b2) ),
inference(resolution,[status(thm)],[d247,d217]) ).
cnf(d249,plain,
( incident(a1,b2c2)
| incident(b1,a2c2)
| incident(a1,b2c2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d248,d199]) ).
cnf(d250,plain,
( incident(b1,a2c2)
| 'point$uequal'(c2,X0)
| 'line$uequal'(b2c2,a1b1)
| ~ incident(X0,b2c2)
| ~ incident(X0,a1b1) ),
inference(resolution,[status(thm)],[d145,c4]) ).
cnf(d251,plain,
( 'point$uequal'(c2,a1)
| 'line$uequal'(b2c2,a1b1)
| incident(b1,a2c2)
| ~ incident(a1,b2c2) ),
inference(resolution,[status(thm)],[d250,c6]) ).
cnf(d252,plain,
( 'point$uequal'(c2,a1)
| 'line$uequal'(b2c2,a1b1)
| incident(b1,a2c2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d249,d251]) ).
cnf(d253,plain,
( ~ incident(a1,X0)
| incident(c2,X0)
| 'line$uequal'(b2c2,a1b1)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d252,c47]) ).
cnf(d254,plain,
( 'line$uequal'(b2c2,a1b1)
| incident(c2,oa)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d253,c21]) ).
cnf(d255,plain,
( ~ incident(X0,b2c2)
| incident(X0,a1b1)
| incident(c2,oa)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d254,c48]) ).
cnf(d256,plain,
( incident(c2,oa)
| incident(b1,a2c2)
| incident(b2,a1b1) ),
inference(resolution,[status(thm)],[d255,c17]) ).
cnf(d257,plain,
( 'point$uequal'(b1,b2)
| 'line$uequal'(a1b1,ob)
| incident(c2,oa)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d256,d62]) ).
cnf(d258,plain,
( 'point$uequal'(b2,b1)
| 'line$uequal'(a1b1,ob)
| incident(c2,oa)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d257,c42]) ).
cnf(d259,plain,
( 'line$uequal'(a1b1,ob)
| incident(c2,oa)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d65,d258]) ).
cnf(d260,plain,
( 'line$uequal'(ob,a1b1)
| incident(c2,oa)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d259,c45]) ).
cnf(d261,plain,
( ~ incident(X0,ob)
| incident(X0,a1b1)
| incident(c2,oa)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d260,c48]) ).
cnf(d262,plain,
( incident(c2,oa)
| incident(b1,a2c2)
| incident(o,a1b1) ),
inference(resolution,[status(thm)],[d261,c19]) ).
cnf(d263,plain,
( 'point$uequal'(c2,o)
| 'line$uequal'(oc,a1b1)
| incident(b1,a2c2)
| incident(c2,oa)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d262,d50]) ).
cnf(d264,plain,
( ~ incident(o,X0)
| incident(c2,X0)
| 'line$uequal'(oc,a1b1)
| incident(c2,oa)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d263,c47]) ).
cnf(d265,plain,
( 'line$uequal'(oc,a1b1)
| incident(c2,oa)
| incident(c2,oa)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d264,c18]) ).
cnf(d266,plain,
( ~ incident(X0,oc)
| incident(X0,a1b1)
| incident(c2,oa)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d265,c48]) ).
cnf(d267,plain,
( incident(c2,oa)
| incident(b1,a2c2)
| incident(c1,a1b1) ),
inference(resolution,[status(thm)],[d266,c25]) ).
cnf(d268,plain,
( incident(c2,oa)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d76,d267]) ).
cnf(d269,plain,
( 'point$uequal'(a2,c2)
| 'line$uequal'(a2c2,oa)
| ~ incident(c2,a2c2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d268,d48]) ).
cnf(d270,plain,
( 'point$uequal'(a2,c2)
| 'line$uequal'(a2c2,oa)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[c13,d269]) ).
cnf(d271,plain,
( ~ incident(c2,X0)
| incident(a2,X0)
| 'line$uequal'(a2c2,oa)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d270,c47]) ).
cnf(d272,plain,
( 'line$uequal'(a2c2,oa)
| incident(a2,b2c2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d271,c16]) ).
cnf(d273,plain,
( 'line$uequal'(a2c2,oa)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d84,d272]) ).
cnf(d274,plain,
( 'line$uequal'(oa,a2c2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d273,c45]) ).
cnf(d275,plain,
( ~ incident(X0,oa)
| incident(X0,a2c2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d274,c48]) ).
cnf(d276,plain,
( incident(b1,a2c2)
| incident(a1,a2c2) ),
inference(resolution,[status(thm)],[d275,c21]) ).
cnf(d277,plain,
( 'point$uequal'(ac,a1)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d276,d47]) ).
cnf(d278,plain,
( ~ incident(a1,X0)
| incident(ac,X0)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d277,c47]) ).
cnf(d279,plain,
( incident(b1,a2c2)
| incident(b1,a2c2)
| incident(ac,b2c2) ),
inference(resolution,[status(thm)],[d278,d249]) ).
cnf(d280,plain,
( incident(b1,a2c2)
| incident(o,a2c2) ),
inference(resolution,[status(thm)],[d275,c18]) ).
cnf(d281,plain,
( 'point$uequal'(o,c2)
| 'line$uequal'(oa,oc)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d268,d99]) ).
cnf(d282,plain,
( ~ incident(c2,X0)
| incident(o,X0)
| 'line$uequal'(oa,oc)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d281,c47]) ).
cnf(d283,plain,
( incident(b1,a2c2)
| 'line$uequal'(oa,oc)
| incident(o,a1b1)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d282,c4]) ).
cnf(d284,plain,
( 'line$uequal'(a2c2,X0)
| ~ 'line$uequal'(oa,X0)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d273,c46]) ).
cnf(d285,plain,
( incident(o,a1b1)
| incident(b1,a2c2)
| 'line$uequal'(a2c2,oc)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d284,d283]) ).
cnf(d286,plain,
( 'line$uequal'(oc,a2c2)
| incident(o,a1b1)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d285,c45]) ).
cnf(d287,plain,
( 'point$uequal'(c1,X0)
| 'line$uequal'(oc,a1c1)
| ~ incident(X0,oc)
| ~ incident(X0,a1c1) ),
inference(resolution,[status(thm)],[d18,c11]) ).
cnf(d288,plain,
( 'point$uequal'(c1,c2)
| 'line$uequal'(oc,a1c1)
| ~ incident(c2,a1c1) ),
inference(resolution,[status(thm)],[d287,c26]) ).
cnf(d289,plain,
( 'line$uequal'(b2c2,a1b1)
| incident(c2,a1c1)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d253,c10]) ).
cnf(d290,plain,
( 'line$uequal'(a1b1,b2c2)
| incident(c2,a1c1)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d289,c45]) ).
cnf(d291,plain,
( ~ incident(X0,a1b1)
| incident(X0,b2c2)
| incident(c2,a1c1)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d290,c48]) ).
cnf(d292,plain,
( incident(c2,a1c1)
| incident(b1,a2c2)
| incident(ab,b2c2) ),
inference(resolution,[status(thm)],[d291,c31]) ).
cnf(d293,plain,
( ~ incident(ac,b2c2)
| incident(c2,a1c1)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d292,d94]) ).
cnf(d294,plain,
( incident(c2,a1c1)
| incident(b1,a2c2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d279,d293]) ).
cnf(d295,plain,
( 'point$uequal'(c1,c2)
| 'line$uequal'(oc,a1c1)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d294,d288]) ).
cnf(d296,plain,
( 'point$uequal'(c2,c1)
| 'line$uequal'(oc,a1c1)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d295,c42]) ).
cnf(d297,plain,
( 'line$uequal'(oc,a1c1)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d8,d296]) ).
cnf(d298,plain,
( 'line$uequal'(a1c1,oc)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d297,c45]) ).
cnf(d299,plain,
( 'line$uequal'(a1c1,X0)
| ~ 'line$uequal'(oc,X0)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d298,c46]) ).
cnf(d300,plain,
( incident(o,a1b1)
| incident(b1,a2c2)
| 'line$uequal'(a1c1,a2c2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d299,d286]) ).
cnf(d301,plain,
( incident(o,a1b1)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d31,d300]) ).
cnf(d302,plain,
( 'point$uequal'(b1,o)
| 'line$uequal'(a1b1,ob)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d301,d96]) ).
cnf(d303,plain,
( ~ incident(o,X0)
| incident(b1,X0)
| 'line$uequal'(a1b1,ob)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d302,c47]) ).
cnf(d304,plain,
( incident(b1,a2c2)
| 'line$uequal'(a1b1,ob)
| incident(b1,a2c2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d303,d280]) ).
cnf(d305,plain,
( 'line$uequal'(ob,a1b1)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d304,c45]) ).
cnf(d306,plain,
( ~ incident(X0,ob)
| incident(X0,a1b1)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d305,c48]) ).
cnf(d307,plain,
( incident(b1,a2c2)
| incident(b2,a1b1) ),
inference(resolution,[status(thm)],[d306,c24]) ).
cnf(d308,plain,
( 'point$uequal'(ab,b2)
| ~ incident(b2,a2b2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d307,d3]) ).
cnf(d309,plain,
( 'point$uequal'(ab,b2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[c9,d308]) ).
cnf(d310,plain,
( ~ incident(b2,X0)
| incident(ab,X0)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d309,c47]) ).
cnf(d311,plain,
( incident(b1,a2c2)
| incident(ab,b2c2) ),
inference(resolution,[status(thm)],[d310,c17]) ).
cnf(d312,plain,
( ~ incident(ac,b2c2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d311,d94]) ).
cnf(d313,plain,
( incident(b1,a2c2)
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[d312,d279]) ).
cnf(d314,plain,
( 'point$uequal'(a2,b1)
| 'line$uequal'(a2c2,b1c1)
| incident(c1,a2b2) ),
inference(resolution,[status(thm)],[d313,d28]) ).
cnf(d315,plain,
( ~ incident(b1,X0)
| incident(a2,X0)
| 'line$uequal'(a2c2,b1c1)
| incident(c1,a2b2) ),
inference(resolution,[status(thm)],[d314,c47]) ).
cnf(d316,plain,
( 'line$uequal'(a2c2,b1c1)
| incident(a2,a1b1)
| incident(c1,a2b2) ),
inference(resolution,[status(thm)],[d315,c7]) ).
cnf(d317,plain,
( ~ incident(X0,a2c2)
| incident(X0,b1c1)
| incident(a2,a1b1)
| incident(c1,a2b2) ),
inference(resolution,[status(thm)],[d316,c48]) ).
cnf(d318,plain,
( incident(a2,a1b1)
| incident(c1,a2b2)
| incident(c2,b1c1) ),
inference(resolution,[status(thm)],[d317,c13]) ).
cnf(d319,plain,
( 'point$uequal'(a1,a2)
| 'line$uequal'(oa,a1b1)
| incident(c2,b1c1)
| incident(c1,a2b2) ),
inference(resolution,[status(thm)],[d318,d25]) ).
cnf(d320,plain,
( 'point$uequal'(a2,a1)
| 'line$uequal'(oa,a1b1)
| incident(c2,b1c1)
| incident(c1,a2b2) ),
inference(resolution,[status(thm)],[d319,c42]) ).
cnf(d321,plain,
( 'line$uequal'(oa,a1b1)
| incident(c2,b1c1)
| incident(c1,a2b2) ),
inference(resolution,[status(thm)],[d203,d320]) ).
cnf(d322,plain,
( ~ incident(X0,oa)
| incident(X0,a1b1)
| incident(c2,b1c1)
| incident(c1,a2b2) ),
inference(resolution,[status(thm)],[d321,c48]) ).
cnf(d323,plain,
( incident(c2,b1c1)
| incident(c1,a2b2)
| incident(o,a1b1) ),
inference(resolution,[status(thm)],[d322,c18]) ).
cnf(d324,plain,
( 'point$uequal'(ab,o)
| ~ incident(o,a2b2)
| incident(c2,b1c1)
| incident(c1,a2b2) ),
inference(resolution,[status(thm)],[d323,d3]) ).
cnf(d325,plain,
( 'point$uequal'(b2,X0)
| 'line$uequal'(ob,X1)
| ~ incident(b2,X1)
| ~ incident(X0,ob)
| ~ incident(X0,X1) ),
inference(resolution,[status(thm)],[c49,c24]) ).
cnf(d326,plain,
( 'point$uequal'(b2,X0)
| 'line$uequal'(ob,a2b2)
| ~ incident(X0,ob)
| ~ incident(X0,a2b2) ),
inference(resolution,[status(thm)],[d325,c9]) ).
cnf(d327,plain,
( 'line$uequal'(a2c2,b1c1)
| incident(a2,ob)
| incident(c1,a2b2) ),
inference(resolution,[status(thm)],[d315,c23]) ).
cnf(d328,plain,
( ~ incident(X0,a2c2)
| incident(X0,b1c1)
| incident(a2,ob)
| incident(c1,a2b2) ),
inference(resolution,[status(thm)],[d327,c48]) ).
cnf(d329,plain,
( incident(a2,ob)
| incident(c1,a2b2)
| incident(c2,b1c1) ),
inference(resolution,[status(thm)],[d328,c13]) ).
cnf(d330,plain,
( 'point$uequal'(b2,a2)
| 'line$uequal'(ob,a2b2)
| ~ incident(a2,a2b2)
| incident(c2,b1c1)
| incident(c1,a2b2) ),
inference(resolution,[status(thm)],[d329,d326]) ).
cnf(d331,plain,
( 'point$uequal'(b2,a2)
| 'line$uequal'(ob,a2b2)
| incident(c2,b1c1)
| incident(c1,a2b2) ),
inference(resolution,[status(thm)],[c8,d330]) ).
cnf(d332,plain,
( 'point$uequal'(a2,b2)
| 'line$uequal'(ob,a2b2)
| incident(c2,b1c1)
| incident(c1,a2b2) ),
inference(resolution,[status(thm)],[d331,c42]) ).
cnf(d333,plain,
( ~ incident(b2,X0)
| incident(a2,X0)
| 'line$uequal'(ob,a2b2)
| incident(c2,b1c1)
| incident(c1,a2b2) ),
inference(resolution,[status(thm)],[d332,c47]) ).
cnf(d334,plain,
( 'line$uequal'(ob,a2b2)
| incident(a2,b2c2)
| incident(c2,b1c1)
| incident(c1,a2b2) ),
inference(resolution,[status(thm)],[d333,c17]) ).
cnf(d335,plain,
( 'line$uequal'(ob,a2b2)
| incident(c2,b1c1)
| incident(c1,a2b2) ),
inference(resolution,[status(thm)],[d84,d334]) ).
cnf(d336,plain,
( ~ incident(X0,ob)
| incident(X0,a2b2)
| incident(c2,b1c1)
| incident(c1,a2b2) ),
inference(resolution,[status(thm)],[d335,c48]) ).
cnf(d337,plain,
( incident(c2,b1c1)
| incident(c1,a2b2)
| incident(o,a2b2) ),
inference(resolution,[status(thm)],[d336,c19]) ).
cnf(d338,plain,
( 'point$uequal'(ab,o)
| incident(c2,b1c1)
| incident(c1,a2b2)
| incident(c2,b1c1)
| incident(c1,a2b2) ),
inference(resolution,[status(thm)],[d337,d324]) ).
cnf(d339,plain,
( ~ incident(o,X0)
| incident(ab,X0)
| incident(c2,b1c1)
| incident(c1,a2b2) ),
inference(resolution,[status(thm)],[d338,c47]) ).
cnf(d340,plain,
( incident(c2,b1c1)
| incident(c1,a2b2)
| incident(ab,oc) ),
inference(resolution,[status(thm)],[d339,c20]) ).
cnf(d341,plain,
( ~ incident(ac,oc)
| ~ incident(bc,oc)
| incident(c2,b1c1)
| incident(c1,a2b2) ),
inference(resolution,[status(thm)],[d340,d22]) ).
cnf(d342,plain,
( 'point$uequal'(ab,a2)
| ~ incident(a2,a2b2)
| incident(c2,b1c1)
| incident(c1,a2b2) ),
inference(resolution,[status(thm)],[d318,d3]) ).
cnf(d343,plain,
( 'point$uequal'(ab,a2)
| incident(c2,b1c1)
| incident(c1,a2b2) ),
inference(resolution,[status(thm)],[c8,d342]) ).
cnf(d344,plain,
( ~ incident(a2,X0)
| incident(ab,X0)
| incident(c2,b1c1)
| incident(c1,a2b2) ),
inference(resolution,[status(thm)],[d343,c47]) ).
cnf(d345,plain,
( incident(c1,a2b2)
| incident(c2,b1c1)
| incident(c1,a2b2)
| incident(ab,b1c1) ),
inference(resolution,[status(thm)],[d344,c5]) ).
cnf(d346,plain,
( 'point$uequal'(o,ab)
| incident(c2,b1c1)
| incident(c1,a2b2) ),
inference(resolution,[status(thm)],[d338,c42]) ).
cnf(d347,plain,
( ~ incident(ab,X0)
| incident(o,X0)
| incident(c2,b1c1)
| incident(c1,a2b2) ),
inference(resolution,[status(thm)],[d346,c47]) ).
cnf(d348,plain,
( incident(c2,b1c1)
| incident(c1,a2b2)
| incident(o,b1c1)
| incident(c2,b1c1)
| incident(c1,a2b2) ),
inference(resolution,[status(thm)],[d347,d345]) ).
cnf(d349,plain,
( 'point$uequal'(c2,X0)
| 'line$uequal'(oc,a2c2)
| ~ incident(X0,oc)
| ~ incident(X0,a2c2) ),
inference(resolution,[status(thm)],[d5,c13]) ).
cnf(d350,plain,
( 'point$uequal'(c2,o)
| 'line$uequal'(oc,a2c2)
| ~ incident(o,a2c2) ),
inference(resolution,[status(thm)],[d349,c20]) ).
cnf(d351,plain,
( incident(c2,b1c1)
| incident(c1,a2b2)
| incident(ab,a2c2) ),
inference(resolution,[status(thm)],[d344,c12]) ).
cnf(d352,plain,
( incident(c2,b1c1)
| incident(c1,a2b2)
| incident(o,a2c2)
| incident(c2,b1c1)
| incident(c1,a2b2) ),
inference(resolution,[status(thm)],[d347,d351]) ).
cnf(d353,plain,
( 'point$uequal'(c2,o)
| 'line$uequal'(oc,a2c2)
| incident(c2,b1c1)
| incident(c1,a2b2) ),
inference(resolution,[status(thm)],[d352,d350]) ).
cnf(d354,plain,
( ~ incident(o,X0)
| incident(c2,X0)
| 'line$uequal'(oc,a2c2)
| incident(c2,b1c1)
| incident(c1,a2b2) ),
inference(resolution,[status(thm)],[d353,c47]) ).
cnf(d355,plain,
( incident(c2,b1c1)
| incident(c1,a2b2)
| 'line$uequal'(oc,a2c2)
| incident(c2,b1c1)
| incident(c2,b1c1)
| incident(c1,a2b2) ),
inference(resolution,[status(thm)],[d354,d348]) ).
cnf(d356,plain,
( 'line$uequal'(a2c2,oc)
| incident(c2,b1c1)
| incident(c1,a2b2) ),
inference(resolution,[status(thm)],[d355,c45]) ).
cnf(d357,plain,
( ~ incident(X0,a2c2)
| incident(X0,oc)
| incident(c2,b1c1)
| incident(c1,a2b2) ),
inference(resolution,[status(thm)],[d356,c48]) ).
cnf(d358,plain,
( incident(c2,b1c1)
| incident(c1,a2b2)
| incident(ac,oc) ),
inference(resolution,[status(thm)],[d357,c30]) ).
cnf(d359,plain,
( incident(c2,b1c1)
| incident(c1,a2b2)
| ~ incident(bc,oc)
| incident(c2,b1c1)
| incident(c1,a2b2) ),
inference(resolution,[status(thm)],[d358,d341]) ).
cnf(d360,plain,
( 'point$uequal'(c1,X0)
| 'line$uequal'(b1c1,X1)
| ~ incident(c1,X1)
| ~ incident(X0,b1c1)
| ~ incident(X0,X1) ),
inference(resolution,[status(thm)],[c49,c14]) ).
cnf(d361,plain,
( 'point$uequal'(c1,X0)
| 'line$uequal'(b1c1,oc)
| ~ incident(X0,b1c1)
| ~ incident(X0,oc) ),
inference(resolution,[status(thm)],[d360,c25]) ).
cnf(d362,plain,
( 'point$uequal'(c1,o)
| 'line$uequal'(b1c1,oc)
| ~ incident(o,b1c1) ),
inference(resolution,[status(thm)],[d361,c20]) ).
cnf(d363,plain,
( 'point$uequal'(c1,o)
| 'line$uequal'(b1c1,oc)
| incident(c2,b1c1)
| incident(c1,a2b2) ),
inference(resolution,[status(thm)],[d348,d362]) ).
cnf(d364,plain,
( ~ incident(o,X0)
| incident(c1,X0)
| 'line$uequal'(b1c1,oc)
| incident(c2,b1c1)
| incident(c1,a2b2) ),
inference(resolution,[status(thm)],[d363,c47]) ).
cnf(d365,plain,
( incident(c2,b1c1)
| incident(c1,a2b2)
| 'line$uequal'(b1c1,oc)
| incident(c2,b1c1)
| incident(c1,a2b2)
| incident(c1,a2b2) ),
inference(resolution,[status(thm)],[d364,d337]) ).
cnf(d366,plain,
( ~ incident(X0,b1c1)
| incident(X0,oc)
| incident(c2,b1c1)
| incident(c1,a2b2) ),
inference(resolution,[status(thm)],[d365,c48]) ).
cnf(d367,plain,
( incident(c2,b1c1)
| incident(c1,a2b2)
| incident(bc,oc) ),
inference(resolution,[status(thm)],[d366,c27]) ).
cnf(d368,plain,
( incident(c2,b1c1)
| incident(c1,a2b2)
| incident(c2,b1c1)
| incident(c1,a2b2) ),
inference(resolution,[status(thm)],[d367,d359]) ).
cnf(d369,plain,
( 'point$uequal'(c1,c2)
| 'line$uequal'(oc,b1c1)
| incident(c1,a2b2) ),
inference(resolution,[status(thm)],[d368,d20]) ).
cnf(d370,plain,
( 'point$uequal'(c2,c1)
| 'line$uequal'(oc,b1c1)
| incident(c1,a2b2) ),
inference(resolution,[status(thm)],[d369,c42]) ).
cnf(d371,plain,
( 'line$uequal'(oc,b1c1)
| incident(c1,a2b2) ),
inference(resolution,[status(thm)],[d8,d370]) ).
cnf(d372,plain,
( ~ incident(X0,oc)
| incident(X0,b1c1)
| incident(c1,a2b2) ),
inference(resolution,[status(thm)],[d371,c48]) ).
cnf(d373,plain,
( 'line$uequal'(b1c1,oc)
| incident(c1,a2b2) ),
inference(resolution,[status(thm)],[d371,c45]) ).
cnf(d374,plain,
( ~ incident(X0,b1c1)
| incident(X0,oc)
| incident(c1,a2b2) ),
inference(resolution,[status(thm)],[d373,c48]) ).
cnf(d375,plain,
( incident(c1,a2b2)
| incident(c1,a2b2)
| incident(a2,oc) ),
inference(resolution,[status(thm)],[d374,c5]) ).
cnf(d376,plain,
( 'point$uequal'(a2,X0)
| 'line$uequal'(oa,oc)
| ~ incident(X0,oa)
| ~ incident(X0,oc)
| incident(c1,a2b2) ),
inference(resolution,[status(thm)],[d375,d173]) ).
cnf(d377,plain,
( 'point$uequal'(a2,c2)
| 'line$uequal'(oa,oc)
| incident(c1,a2b2)
| ~ incident(c2,oa) ),
inference(resolution,[status(thm)],[d376,c26]) ).
cnf(d378,plain,
( ~ incident(a2,ob)
| ~ incident(c2,ob) ),
inference(resolution,[status(thm)],[d82,c24]) ).
cnf(d379,plain,
( incident(c1,a2b2)
| 'point$uequal'(a2,X0)
| 'line$uequal'(b1c1,X1)
| ~ incident(a2,X1)
| ~ incident(X0,b1c1)
| ~ incident(X0,X1) ),
inference(resolution,[status(thm)],[c49,c5]) ).
cnf(d380,plain,
( 'point$uequal'(a2,X0)
| 'line$uequal'(b1c1,oa)
| incident(c1,a2b2)
| ~ incident(X0,b1c1)
| ~ incident(X0,oa) ),
inference(resolution,[status(thm)],[d379,c22]) ).
cnf(d381,plain,
( 'point$uequal'(a2,o)
| 'line$uequal'(b1c1,oa)
| incident(c1,a2b2)
| ~ incident(o,b1c1) ),
inference(resolution,[status(thm)],[d380,c18]) ).
cnf(d382,plain,
( incident(c1,a2b2)
| incident(o,b1c1) ),
inference(resolution,[status(thm)],[d372,c20]) ).
cnf(d383,plain,
( 'point$uequal'(a2,o)
| 'line$uequal'(b1c1,oa)
| incident(c1,a2b2)
| incident(c1,a2b2) ),
inference(resolution,[status(thm)],[d382,d381]) ).
cnf(d384,plain,
( ~ incident(o,X0)
| incident(a2,X0)
| 'line$uequal'(b1c1,oa)
| incident(c1,a2b2) ),
inference(resolution,[status(thm)],[d383,c47]) ).
cnf(d385,plain,
( 'line$uequal'(b1c1,oa)
| incident(a2,ob)
| incident(c1,a2b2) ),
inference(resolution,[status(thm)],[d384,c19]) ).
cnf(d386,plain,
( ~ incident(X0,b1c1)
| incident(X0,oa)
| incident(a2,ob)
| incident(c1,a2b2) ),
inference(resolution,[status(thm)],[d385,c48]) ).
cnf(d387,plain,
( incident(c1,a2b2)
| incident(a2,ob)
| incident(c1,a2b2)
| incident(c2,oa) ),
inference(resolution,[status(thm)],[d386,d368]) ).
cnf(d388,plain,
( ~ incident(c2,ob)
| incident(c2,oa)
| incident(c1,a2b2) ),
inference(resolution,[status(thm)],[d387,d378]) ).
cnf(d389,plain,
( 'point$uequal'(bc,c2)
| ~ incident(c2,b2c2)
| incident(c1,a2b2) ),
inference(resolution,[status(thm)],[d368,d36]) ).
cnf(d390,plain,
( 'point$uequal'(bc,c2)
| incident(c1,a2b2) ),
inference(resolution,[status(thm)],[c16,d389]) ).
cnf(d391,plain,
( 'point$uequal'(c2,bc)
| incident(c1,a2b2) ),
inference(resolution,[status(thm)],[d390,c42]) ).
cnf(d392,plain,
( ~ incident(bc,X0)
| incident(c2,X0)
| incident(c1,a2b2) ),
inference(resolution,[status(thm)],[d391,c47]) ).
cnf(d393,plain,
( ~ incident(c2,X0)
| incident(bc,X0)
| incident(c1,a2b2) ),
inference(resolution,[status(thm)],[d390,c47]) ).
cnf(d394,plain,
( incident(c1,a2b2)
| incident(bc,a2c2) ),
inference(resolution,[status(thm)],[d393,c13]) ).
cnf(d395,plain,
'line$uequal'(a2c2,a2c2),
inference(resolution,[status(thm)],[c44,c12]) ).
cnf(d396,plain,
( ~ incident(ab,a2c2)
| ~ incident(ac,a2c2)
| ~ incident(bc,a2c2) ),
inference(resolution,[status(thm)],[d395,d10]) ).
cnf(d397,plain,
( ~ incident(ab,a2c2)
| ~ incident(bc,a2c2) ),
inference(resolution,[status(thm)],[c30,d396]) ).
cnf(d398,plain,
( 'point$uequal'(a2,bc)
| 'line$uequal'(a2c2,b1c1)
| incident(c1,a2b2)
| ~ incident(bc,a2c2) ),
inference(resolution,[status(thm)],[d27,c27]) ).
cnf(d399,plain,
( 'point$uequal'(a2,bc)
| 'line$uequal'(a2c2,b1c1)
| incident(c1,a2b2)
| incident(c1,a2b2) ),
inference(resolution,[status(thm)],[d394,d398]) ).
cnf(d400,plain,
( ~ incident(bc,X0)
| incident(a2,X0)
| 'line$uequal'(a2c2,b1c1)
| incident(c1,a2b2) ),
inference(resolution,[status(thm)],[d399,c47]) ).
cnf(d401,plain,
( 'line$uequal'(a2c2,b1c1)
| incident(a2,b2c2)
| incident(c1,a2b2) ),
inference(resolution,[status(thm)],[d400,c28]) ).
cnf(d402,plain,
( 'line$uequal'(a2c2,b1c1)
| incident(c1,a2b2) ),
inference(resolution,[status(thm)],[d84,d401]) ).
cnf(d403,plain,
( 'line$uequal'(b1c1,a2c2)
| incident(c1,a2b2) ),
inference(resolution,[status(thm)],[d402,c45]) ).
cnf(d404,plain,
( ~ incident(X0,b1c1)
| incident(X0,a2c2)
| incident(c1,a2b2) ),
inference(resolution,[status(thm)],[d403,c48]) ).
cnf(d405,plain,
( incident(c1,a2b2)
| incident(c1,a2b2)
| incident(o,a2c2) ),
inference(resolution,[status(thm)],[d404,d382]) ).
cnf(d406,plain,
( 'point$uequal'(o,a2)
| 'line$uequal'(b1c1,oa)
| incident(c1,a2b2) ),
inference(resolution,[status(thm)],[d383,c42]) ).
cnf(d407,plain,
( ~ incident(a2,X0)
| incident(o,X0)
| 'line$uequal'(b1c1,oa)
| incident(c1,a2b2) ),
inference(resolution,[status(thm)],[d406,c47]) ).
cnf(d408,plain,
( 'line$uequal'(b1c1,oa)
| incident(o,a2b2)
| incident(c1,a2b2) ),
inference(resolution,[status(thm)],[d407,c8]) ).
cnf(d409,plain,
( ~ incident(X0,b1c1)
| incident(X0,oa)
| incident(o,a2b2)
| incident(c1,a2b2) ),
inference(resolution,[status(thm)],[d408,c48]) ).
cnf(d410,plain,
( incident(o,a2b2)
| incident(c1,a2b2)
| incident(bc,oa) ),
inference(resolution,[status(thm)],[d409,c27]) ).
cnf(d411,plain,
( 'point$uequal'(b1,X0)
| 'line$uequal'(b1c1,X1)
| ~ incident(b1,X1)
| ~ incident(X0,b1c1)
| ~ incident(X0,X1) ),
inference(resolution,[status(thm)],[c49,c15]) ).
cnf(d412,plain,
( 'point$uequal'(b1,X0)
| 'line$uequal'(b1c1,ob)
| ~ incident(X0,b1c1)
| ~ incident(X0,ob) ),
inference(resolution,[status(thm)],[d411,c23]) ).
cnf(d413,plain,
( 'point$uequal'(b1,o)
| 'line$uequal'(b1c1,ob)
| ~ incident(o,b1c1) ),
inference(resolution,[status(thm)],[d412,c19]) ).
cnf(d414,plain,
( 'point$uequal'(b1,o)
| 'line$uequal'(b1c1,ob)
| incident(c1,a2b2) ),
inference(resolution,[status(thm)],[d382,d413]) ).
cnf(d415,plain,
( 'point$uequal'(o,b1)
| 'line$uequal'(b1c1,ob)
| incident(c1,a2b2) ),
inference(resolution,[status(thm)],[d414,c42]) ).
cnf(d416,plain,
( ~ incident(b1,X0)
| incident(o,X0)
| 'line$uequal'(b1c1,ob)
| incident(c1,a2b2) ),
inference(resolution,[status(thm)],[d415,c47]) ).
cnf(d417,plain,
( 'line$uequal'(b1c1,ob)
| incident(o,a1b1)
| incident(c1,a2b2) ),
inference(resolution,[status(thm)],[d416,c7]) ).
cnf(d418,plain,
( ~ incident(X0,b1c1)
| incident(X0,ob)
| incident(o,a1b1)
| incident(c1,a2b2) ),
inference(resolution,[status(thm)],[d417,c48]) ).
cnf(d419,plain,
( incident(o,a1b1)
| incident(c1,a2b2)
| incident(bc,ob) ),
inference(resolution,[status(thm)],[d418,c27]) ).
cnf(d420,plain,
( 'point$uequal'(ab,o)
| ~ incident(o,a2b2)
| incident(c1,a2b2)
| incident(bc,ob) ),
inference(resolution,[status(thm)],[d419,d3]) ).
cnf(d421,plain,
( incident(c1,a2b2)
| incident(bc,oa)
| 'point$uequal'(ab,o)
| incident(c1,a2b2)
| incident(bc,ob) ),
inference(resolution,[status(thm)],[d420,d410]) ).
cnf(d422,plain,
( ~ incident(o,X0)
| incident(ab,X0)
| incident(c1,a2b2)
| incident(bc,ob)
| incident(bc,oa) ),
inference(resolution,[status(thm)],[d421,c47]) ).
cnf(d423,plain,
( incident(c1,a2b2)
| incident(c1,a2b2)
| incident(ab,a2c2)
| incident(bc,ob)
| incident(bc,oa) ),
inference(resolution,[status(thm)],[d422,d405]) ).
cnf(d424,plain,
( ~ incident(bc,a2c2)
| incident(c1,a2b2)
| incident(bc,ob)
| incident(bc,oa) ),
inference(resolution,[status(thm)],[d423,d397]) ).
cnf(d425,plain,
( incident(c1,a2b2)
| incident(c1,a2b2)
| incident(bc,ob)
| incident(bc,oa) ),
inference(resolution,[status(thm)],[d424,d394]) ).
cnf(d426,plain,
( incident(c2,ob)
| incident(c1,a2b2)
| incident(c1,a2b2)
| incident(bc,oa) ),
inference(resolution,[status(thm)],[d425,d392]) ).
cnf(d427,plain,
( incident(c2,oa)
| incident(c1,a2b2)
| incident(c2,ob)
| incident(c1,a2b2) ),
inference(resolution,[status(thm)],[d426,d392]) ).
cnf(d428,plain,
( incident(c2,oa)
| incident(c1,a2b2)
| incident(c2,oa)
| incident(c1,a2b2) ),
inference(resolution,[status(thm)],[d427,d388]) ).
cnf(d429,plain,
( 'point$uequal'(a2,c2)
| 'line$uequal'(oa,oc)
| incident(c1,a2b2)
| incident(c1,a2b2) ),
inference(resolution,[status(thm)],[d428,d377]) ).
cnf(d430,plain,
( ~ incident(c2,X0)
| incident(a2,X0)
| 'line$uequal'(oa,oc)
| incident(c1,a2b2) ),
inference(resolution,[status(thm)],[d429,c47]) ).
cnf(d431,plain,
( 'line$uequal'(oa,oc)
| incident(a2,b2c2)
| incident(c1,a2b2) ),
inference(resolution,[status(thm)],[d430,c16]) ).
cnf(d432,plain,
( 'line$uequal'(oa,oc)
| incident(c1,a2b2) ),
inference(resolution,[status(thm)],[d84,d431]) ).
cnf(d433,plain,
( ~ incident(X0,oa)
| incident(X0,oc)
| incident(c1,a2b2) ),
inference(resolution,[status(thm)],[d432,c48]) ).
cnf(d434,plain,
( incident(c1,a2b2)
| incident(a1,oc) ),
inference(resolution,[status(thm)],[d433,c21]) ).
cnf(d435,plain,
( incident(c1,a2b2)
| incident(a1,b1c1)
| incident(c1,a2b2) ),
inference(resolution,[status(thm)],[d434,d372]) ).
cnf(d436,plain,
( ~ incident(c1,b1c1)
| ~ incident(b1,b1c1)
| incident(c1,a2b2) ),
inference(resolution,[status(thm)],[d435,d17]) ).
cnf(d437,plain,
( incident(c1,a2b2)
| ~ incident(b1,b1c1) ),
inference(resolution,[status(thm)],[c14,d436]) ).
cnf(d438,plain,
incident(c1,a2b2),
inference(resolution,[status(thm)],[c15,d437]) ).
cnf(d439,plain,
( 'point$uequal'(b2,c1)
| 'line$uequal'(a2b2,a1c1)
| incident(a1,b2c2) ),
inference(resolution,[status(thm)],[d438,d16]) ).
cnf(d440,plain,
( ~ incident(a1,b2c2)
| ~ incident(c1,a2b2)
| ~ incident(b1,a2c2) ),
inference(resolution,[status(thm)],[c50,c1]) ).
cnf(d441,plain,
( ~ incident(a1,b2c2)
| ~ incident(c1,a2b2) ),
inference(resolution,[status(thm)],[d313,d440]) ).
cnf(d442,plain,
~ incident(a1,b2c2),
inference(resolution,[status(thm)],[d438,d441]) ).
cnf(d443,plain,
( 'point$uequal'(b2,c1)
| 'line$uequal'(a2b2,a1c1) ),
inference(resolution,[status(thm)],[d442,d439]) ).
cnf(d444,plain,
( 'point$uequal'(c1,b2)
| 'line$uequal'(a2b2,a1c1) ),
inference(resolution,[status(thm)],[d443,c42]) ).
cnf(d445,plain,
( ~ incident(b2,X0)
| incident(c1,X0)
| 'line$uequal'(a2b2,a1c1) ),
inference(resolution,[status(thm)],[d444,c47]) ).
cnf(d446,plain,
( 'line$uequal'(a2b2,a1c1)
| incident(c1,b2c2) ),
inference(resolution,[status(thm)],[d445,c17]) ).
cnf(d447,plain,
( 'line$uequal'(a1c1,a2b2)
| incident(c1,b2c2) ),
inference(resolution,[status(thm)],[d446,c45]) ).
cnf(d448,plain,
( ~ incident(X0,a1c1)
| incident(X0,a2b2)
| incident(c1,b2c2) ),
inference(resolution,[status(thm)],[d447,c48]) ).
cnf(d449,plain,
( incident(c1,b2c2)
| incident(ac,a2b2) ),
inference(resolution,[status(thm)],[d448,c29]) ).
cnf(d450,plain,
( ~ incident(bc,a2b2)
| incident(c1,b2c2) ),
inference(resolution,[status(thm)],[d449,d13]) ).
cnf(d451,plain,
( incident(a1,b2c2)
| ~ incident(a2,a1c1)
| ~ incident(c2,a1c1) ),
inference(resolution,[status(thm)],[d82,c3]) ).
cnf(d452,plain,
( ~ incident(a2,a1c1)
| ~ incident(c2,a1c1) ),
inference(resolution,[status(thm)],[d442,d451]) ).
cnf(d453,plain,
( 'line$uequal'(a2b2,a1c1)
| incident(c1,ob) ),
inference(resolution,[status(thm)],[d445,c24]) ).
cnf(d454,plain,
( ~ incident(X0,a2b2)
| incident(X0,a1c1)
| incident(c1,ob) ),
inference(resolution,[status(thm)],[d453,c48]) ).
cnf(d455,plain,
( incident(c1,ob)
| incident(a2,a1c1) ),
inference(resolution,[status(thm)],[d454,c8]) ).
cnf(d456,plain,
( ~ incident(c2,a1c1)
| incident(c1,ob) ),
inference(resolution,[status(thm)],[d455,d452]) ).
cnf(d457,plain,
( 'point$uequal'(a2,a1)
| 'line$uequal'(oa,a2b2)
| ~ incident(a1,a2b2) ),
inference(resolution,[status(thm)],[d174,c21]) ).
cnf(d458,plain,
( 'line$uequal'(oa,a2b2)
| ~ incident(a1,a2b2) ),
inference(resolution,[status(thm)],[d203,d457]) ).
cnf(d459,plain,
( 'line$uequal'(a1c1,a2b2)
| incident(c1,ob) ),
inference(resolution,[status(thm)],[d453,c45]) ).
cnf(d460,plain,
( ~ incident(X0,a1c1)
| incident(X0,a2b2)
| incident(c1,ob) ),
inference(resolution,[status(thm)],[d459,c48]) ).
cnf(d461,plain,
( incident(c1,ob)
| incident(a1,a2b2) ),
inference(resolution,[status(thm)],[d460,c10]) ).
cnf(d462,plain,
( 'line$uequal'(oa,a2b2)
| incident(c1,ob) ),
inference(resolution,[status(thm)],[d461,d458]) ).
cnf(d463,plain,
( ~ incident(X0,oa)
| incident(X0,a2b2)
| incident(c1,ob) ),
inference(resolution,[status(thm)],[d462,c48]) ).
cnf(d464,plain,
( incident(c1,ob)
| incident(o,a2b2) ),
inference(resolution,[status(thm)],[d463,c18]) ).
cnf(d465,plain,
( incident(c1,ob)
| incident(o,a1c1)
| incident(c1,ob) ),
inference(resolution,[status(thm)],[d464,d454]) ).
cnf(d466,plain,
( 'point$uequal'(c1,o)
| 'line$uequal'(a1c1,oc)
| incident(c1,ob) ),
inference(resolution,[status(thm)],[d465,d233]) ).
cnf(d467,plain,
( ~ incident(o,X0)
| incident(c1,X0)
| 'line$uequal'(a1c1,oc)
| incident(c1,ob) ),
inference(resolution,[status(thm)],[d466,c47]) ).
cnf(d468,plain,
( 'line$uequal'(a1c1,oc)
| incident(c1,ob)
| incident(c1,ob) ),
inference(resolution,[status(thm)],[d467,c19]) ).
cnf(d469,plain,
( 'line$uequal'(oc,a1c1)
| incident(c1,ob) ),
inference(resolution,[status(thm)],[d468,c45]) ).
cnf(d470,plain,
( ~ incident(X0,oc)
| incident(X0,a1c1)
| incident(c1,ob) ),
inference(resolution,[status(thm)],[d469,c48]) ).
cnf(d471,plain,
( incident(c1,ob)
| incident(c2,a1c1) ),
inference(resolution,[status(thm)],[d470,c26]) ).
cnf(d472,plain,
( incident(c1,ob)
| incident(c1,ob) ),
inference(resolution,[status(thm)],[d471,d456]) ).
cnf(d473,plain,
( 'point$uequal'(b1,c1)
| 'line$uequal'(b1c1,ob)
| ~ incident(c1,b1c1) ),
inference(resolution,[status(thm)],[d472,d412]) ).
cnf(d474,plain,
( 'point$uequal'(b1,c1)
| 'line$uequal'(b1c1,ob) ),
inference(resolution,[status(thm)],[c14,d473]) ).
cnf(d475,plain,
( ~ incident(c1,X0)
| incident(b1,X0)
| 'line$uequal'(b1c1,ob) ),
inference(resolution,[status(thm)],[d474,c47]) ).
cnf(d476,plain,
( 'line$uequal'(b1c1,ob)
| incident(b1,a1c1) ),
inference(resolution,[status(thm)],[d475,c11]) ).
cnf(d477,plain,
'line$uequal'(b1c1,ob),
inference(resolution,[status(thm)],[d231,d476]) ).
cnf(d478,plain,
'line$uequal'(ob,b1c1),
inference(resolution,[status(thm)],[d477,c45]) ).
cnf(d479,plain,
( ~ incident(X0,ob)
| incident(X0,b1c1) ),
inference(resolution,[status(thm)],[d478,c48]) ).
cnf(d480,plain,
incident(b2,b1c1),
inference(resolution,[status(thm)],[d479,c24]) ).
cnf(d481,plain,
( 'point$uequal'(bc,b2)
| ~ incident(b2,b2c2) ),
inference(resolution,[status(thm)],[d480,d36]) ).
cnf(d482,plain,
'point$uequal'(bc,b2),
inference(resolution,[status(thm)],[c17,d481]) ).
cnf(d483,plain,
( ~ incident(b2,X0)
| incident(bc,X0) ),
inference(resolution,[status(thm)],[d482,c47]) ).
cnf(d484,plain,
incident(bc,a2b2),
inference(resolution,[status(thm)],[d483,c9]) ).
cnf(d485,plain,
incident(c1,b2c2),
inference(resolution,[status(thm)],[d484,d450]) ).
cnf(d486,plain,
'line$uequal'(oc,b2c2),
inference(resolution,[status(thm)],[d485,d9]) ).
cnf(d487,plain,
( ~ incident(X0,oc)
| incident(X0,b2c2) ),
inference(resolution,[status(thm)],[d486,c48]) ).
cnf(d488,plain,
incident(o,b2c2),
inference(resolution,[status(thm)],[d487,c20]) ).
cnf(d489,plain,
incident(o,b1c1),
inference(resolution,[status(thm)],[d479,c19]) ).
cnf(d490,plain,
( 'point$uequal'(bc,o)
| ~ incident(o,b2c2) ),
inference(resolution,[status(thm)],[d489,d36]) ).
cnf(d491,plain,
'point$uequal'(bc,o),
inference(resolution,[status(thm)],[d488,d490]) ).
cnf(d492,plain,
'point$uequal'(o,bc),
inference(resolution,[status(thm)],[d491,c42]) ).
cnf(d493,plain,
( ~ incident(bc,X0)
| incident(o,X0) ),
inference(resolution,[status(thm)],[d492,c47]) ).
cnf(d494,plain,
incident(o,a2b2),
inference(resolution,[status(thm)],[d493,d484]) ).
cnf(d495,plain,
( 'point$uequal'(a2,o)
| 'line$uequal'(oa,a2b2) ),
inference(resolution,[status(thm)],[d494,d175]) ).
cnf(d496,plain,
( ~ incident(o,X0)
| incident(a2,X0)
| 'line$uequal'(oa,a2b2) ),
inference(resolution,[status(thm)],[d495,c47]) ).
cnf(d497,plain,
( 'line$uequal'(oa,a2b2)
| incident(a2,b2c2) ),
inference(resolution,[status(thm)],[d496,d488]) ).
cnf(d498,plain,
'line$uequal'(oa,a2b2),
inference(resolution,[status(thm)],[d84,d497]) ).
cnf(d499,plain,
( ~ incident(X0,oa)
| incident(X0,a2b2) ),
inference(resolution,[status(thm)],[d498,c48]) ).
cnf(d500,plain,
incident(a1,a2b2),
inference(resolution,[status(thm)],[d499,c21]) ).
cnf(d501,plain,
'point$uequal'(ab,a1),
inference(resolution,[status(thm)],[d500,d4]) ).
cnf(d502,plain,
( ~ incident(a1,X0)
| incident(ab,X0) ),
inference(resolution,[status(thm)],[d501,c47]) ).
cnf(d503,plain,
incident(ab,a1c1),
inference(resolution,[status(thm)],[d502,c10]) ).
cnf(d504,plain,
'line$uequal'(a1c1,a1c1),
inference(resolution,[status(thm)],[c44,c11]) ).
cnf(d505,plain,
( ~ incident(ab,a1c1)
| ~ incident(ac,a1c1)
| ~ incident(bc,a1c1) ),
inference(resolution,[status(thm)],[d504,d10]) ).
cnf(d506,plain,
( ~ incident(ab,a1c1)
| ~ incident(bc,a1c1) ),
inference(resolution,[status(thm)],[c29,d505]) ).
cnf(d507,plain,
incident(b2,a1c1),
inference(resolution,[status(thm)],[d442,c3]) ).
cnf(d508,plain,
incident(bc,a1c1),
inference(resolution,[status(thm)],[d483,d507]) ).
cnf(d509,plain,
~ incident(ab,a1c1),
inference(resolution,[status(thm)],[d508,d506]) ).
cnf(d510,plain,
$false,
inference(resolution,[status(thm)],[d509,d503]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO169+1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.04 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 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 : Fri Sep 25 12:59:59 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.36 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 136.74/17.91 % SZS status Theorem for theBenchmark.p
% 136.74/17.91 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
%------------------------------------------------------------------------------