%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : GEO169+1 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n004.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:17:13 AM UTC 2026
% Result : Theorem 74.55s 10.19s
% Output : CNFRefutation 74.55s
% Verified :
% SZS Type : Refutation
% Derivation depth : 166
% Number of leaves : 50
% Syntax : Number of formulae : 560 ( 128 unt; 0 def)
% Number of atoms : 1586 ( 0 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 1523 ( 497 ~; 989 |; 18 &)
% ( 0 <=>; 19 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 3 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 5 ( 4 usr; 2 prp; 0-2 aty)
% Number of functors : 19 ( 19 usr; 19 con; 0-0 aty)
% Number of variables : 215 ( 1 sgn 25 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(goal_normal,axiom,
! [A] :
( ( incident(ab,A)
& incident(ac,A)
& incident(bc,A)
& line_equal(A,A) )
=> goal ),
file('theBenchmark.p',goal_normal) ).
fof(t1in2,axiom,
( ( incident(c1,a2b2)
& incident(b1,a2c2)
& incident(a1,b2c2) )
=> goal ),
file('theBenchmark.p',t1in2) ).
fof(t2in1,axiom,
( ( incident(c2,a1b1)
& incident(b2,a1c1)
& incident(a2,b1c1) )
=> goal ),
file('theBenchmark.p',t2in1) ).
fof(triangle1,axiom,
! [A] :
( ( incident(c1,A)
& incident(b1,A)
& incident(a1,A) )
=> goal ),
file('theBenchmark.p',triangle1) ).
fof(triangle2,axiom,
! [A] :
( ( incident(c2,A)
& incident(b2,A)
& incident(a2,A) )
=> goal ),
file('theBenchmark.p',triangle2) ).
fof(notaa,axiom,
( point_equal(a2,a1)
=> goal ),
file('theBenchmark.p',notaa) ).
fof(notbb,axiom,
( point_equal(b2,b1)
=> goal ),
file('theBenchmark.p',notbb) ).
fof(notcc,axiom,
( point_equal(c2,c1)
=> goal ),
file('theBenchmark.p',notcc) ).
fof(notbc,axiom,
( line_equal(b1c1,b2c2)
=> goal ),
file('theBenchmark.p',notbc) ).
fof(notac,axiom,
( line_equal(a1c1,a2c2)
=> goal ),
file('theBenchmark.p',notac) ).
fof(notab,axiom,
( line_equal(a1b1,a2b2)
=> goal ),
file('theBenchmark.p',notab) ).
fof(symmetry_of_point_equal,axiom,
! [A,B] :
( point_equal(A,B)
=> point_equal(B,A) ),
file('theBenchmark.p',symmetry_of_point_equal) ).
fof(transitivity_of_point_equal,axiom,
! [A,B,C] :
( ( point_equal(B,C)
& point_equal(A,B) )
=> point_equal(A,C) ),
file('theBenchmark.p',transitivity_of_point_equal) ).
fof(reflexivity_of_line_equal,axiom,
! [A,B] :
( incident(A,B)
=> line_equal(B,B) ),
file('theBenchmark.p',reflexivity_of_line_equal) ).
fof(symmetry_of_line_equal,axiom,
! [A,B] :
( line_equal(A,B)
=> line_equal(B,A) ),
file('theBenchmark.p',symmetry_of_line_equal) ).
fof(transitivity_of_line_equal,axiom,
! [A,B,C] :
( ( line_equal(B,C)
& line_equal(A,B) )
=> line_equal(A,C) ),
file('theBenchmark.p',transitivity_of_line_equal) ).
fof(pcon,axiom,
! [A,B,C] :
( ( incident(B,C)
& point_equal(A,B) )
=> incident(A,C) ),
file('theBenchmark.p',pcon) ).
fof(lcon,axiom,
! [A,B,C] :
( ( line_equal(B,C)
& incident(A,B) )
=> incident(A,C) ),
file('theBenchmark.p',lcon) ).
fof(unique,axiom,
! [A,B,C,D] :
( ( incident(B,D)
& incident(B,C)
& incident(A,D)
& incident(A,C) )
=> ( line_equal(C,D)
| point_equal(A,B) ) ),
file('theBenchmark.p',unique) ).
fof(goal_to_be_proved,conjecture,
goal,
file('theBenchmark.p',goal_to_be_proved) ).
fof(goal_to_be_proved_neg,negated_conjecture,
~ goal,
inference(assume_negation,[status(cth)],[goal_to_be_proved]) ).
cnf(c_22,plain,
( goal
| ~ incident(ab,A)
| ~ incident(ac,A)
| ~ incident(bc,A)
| ~ line_equal(A,A) ),
inference(clausify,[status(thm)],[goal_normal]) ).
cnf(c_23,plain,
( goal
| ~ incident(c1,a2b2)
| ~ incident(b1,a2c2)
| ~ incident(a1,b2c2) ),
inference(clausify,[status(thm)],[t1in2]) ).
cnf(c_24,plain,
( goal
| ~ incident(c2,a1b1)
| ~ incident(b2,a1c1)
| ~ incident(a2,b1c1) ),
inference(clausify,[status(thm)],[t2in1]) ).
fof(gap_a,axiom,
( incident(b2,a1c1)
| incident(a1,b2c2) ),
file('theBenchmark.p',gap_a) ).
cnf(c_25,plain,
( incident(b2,a1c1)
| incident(a1,b2c2) ),
inference(clausify,[status(thm)],[gap_a]) ).
fof(gap_b,axiom,
( incident(c2,a1b1)
| incident(b1,a2c2) ),
file('theBenchmark.p',gap_b) ).
cnf(c_26,plain,
( incident(c2,a1b1)
| incident(b1,a2c2) ),
inference(clausify,[status(thm)],[gap_b]) ).
fof(gap_c,axiom,
( incident(a2,b1c1)
| incident(c1,a2b2) ),
file('theBenchmark.p',gap_c) ).
cnf(c_27,plain,
( incident(a2,b1c1)
| incident(c1,a2b2) ),
inference(clausify,[status(thm)],[gap_c]) ).
fof(ia1b1,axiom,
incident(a1,a1b1),
file('theBenchmark.p',ia1b1) ).
cnf(c_28,plain,
incident(a1,a1b1),
inference(clausify,[status(thm)],[ia1b1]) ).
fof(ib1a1,axiom,
incident(b1,a1b1),
file('theBenchmark.p',ib1a1) ).
cnf(c_29,plain,
incident(b1,a1b1),
inference(clausify,[status(thm)],[ib1a1]) ).
fof(ia2b2,axiom,
incident(a2,a2b2),
file('theBenchmark.p',ia2b2) ).
cnf(c_30,plain,
incident(a2,a2b2),
inference(clausify,[status(thm)],[ia2b2]) ).
fof(ib2a2,axiom,
incident(b2,a2b2),
file('theBenchmark.p',ib2a2) ).
cnf(c_31,plain,
incident(b2,a2b2),
inference(clausify,[status(thm)],[ib2a2]) ).
fof(ia1c1,axiom,
incident(a1,a1c1),
file('theBenchmark.p',ia1c1) ).
cnf(c_32,plain,
incident(a1,a1c1),
inference(clausify,[status(thm)],[ia1c1]) ).
fof(ic1a1,axiom,
incident(c1,a1c1),
file('theBenchmark.p',ic1a1) ).
cnf(c_33,plain,
incident(c1,a1c1),
inference(clausify,[status(thm)],[ic1a1]) ).
fof(ia2c2,axiom,
incident(a2,a2c2),
file('theBenchmark.p',ia2c2) ).
cnf(c_34,plain,
incident(a2,a2c2),
inference(clausify,[status(thm)],[ia2c2]) ).
fof(ic2a2,axiom,
incident(c2,a2c2),
file('theBenchmark.p',ic2a2) ).
cnf(c_35,plain,
incident(c2,a2c2),
inference(clausify,[status(thm)],[ic2a2]) ).
fof(ic1b1,axiom,
incident(c1,b1c1),
file('theBenchmark.p',ic1b1) ).
cnf(c_36,plain,
incident(c1,b1c1),
inference(clausify,[status(thm)],[ic1b1]) ).
fof(ib1c1,axiom,
incident(b1,b1c1),
file('theBenchmark.p',ib1c1) ).
cnf(c_37,plain,
incident(b1,b1c1),
inference(clausify,[status(thm)],[ib1c1]) ).
fof(ic2b2,axiom,
incident(c2,b2c2),
file('theBenchmark.p',ic2b2) ).
cnf(c_38,plain,
incident(c2,b2c2),
inference(clausify,[status(thm)],[ic2b2]) ).
fof(ib2c2,axiom,
incident(b2,b2c2),
file('theBenchmark.p',ib2c2) ).
cnf(c_39,plain,
incident(b2,b2c2),
inference(clausify,[status(thm)],[ib2c2]) ).
fof(iooa,axiom,
incident(o,oa),
file('theBenchmark.p',iooa) ).
cnf(c_40,plain,
incident(o,oa),
inference(clausify,[status(thm)],[iooa]) ).
fof(ioob,axiom,
incident(o,ob),
file('theBenchmark.p',ioob) ).
cnf(c_41,plain,
incident(o,ob),
inference(clausify,[status(thm)],[ioob]) ).
fof(iooc,axiom,
incident(o,oc),
file('theBenchmark.p',iooc) ).
cnf(c_42,plain,
incident(o,oc),
inference(clausify,[status(thm)],[iooc]) ).
fof(ia1oa,axiom,
incident(a1,oa),
file('theBenchmark.p',ia1oa) ).
cnf(c_43,plain,
incident(a1,oa),
inference(clausify,[status(thm)],[ia1oa]) ).
fof(ia2oa,axiom,
incident(a2,oa),
file('theBenchmark.p',ia2oa) ).
cnf(c_44,plain,
incident(a2,oa),
inference(clausify,[status(thm)],[ia2oa]) ).
fof(ib1ob,axiom,
incident(b1,ob),
file('theBenchmark.p',ib1ob) ).
cnf(c_45,plain,
incident(b1,ob),
inference(clausify,[status(thm)],[ib1ob]) ).
fof(ib2ob,axiom,
incident(b2,ob),
file('theBenchmark.p',ib2ob) ).
cnf(c_46,plain,
incident(b2,ob),
inference(clausify,[status(thm)],[ib2ob]) ).
fof(ic1oc,axiom,
incident(c1,oc),
file('theBenchmark.p',ic1oc) ).
cnf(c_47,plain,
incident(c1,oc),
inference(clausify,[status(thm)],[ic1oc]) ).
fof(ic2oc,axiom,
incident(c2,oc),
file('theBenchmark.p',ic2oc) ).
cnf(c_48,plain,
incident(c2,oc),
inference(clausify,[status(thm)],[ic2oc]) ).
fof(ibc1,axiom,
incident(bc,b1c1),
file('theBenchmark.p',ibc1) ).
cnf(c_49,plain,
incident(bc,b1c1),
inference(clausify,[status(thm)],[ibc1]) ).
fof(ibc2,axiom,
incident(bc,b2c2),
file('theBenchmark.p',ibc2) ).
cnf(c_50,plain,
incident(bc,b2c2),
inference(clausify,[status(thm)],[ibc2]) ).
fof(iac1,axiom,
incident(ac,a1c1),
file('theBenchmark.p',iac1) ).
cnf(c_51,plain,
incident(ac,a1c1),
inference(clausify,[status(thm)],[iac1]) ).
fof(iac2,axiom,
incident(ac,a2c2),
file('theBenchmark.p',iac2) ).
cnf(c_52,plain,
incident(ac,a2c2),
inference(clausify,[status(thm)],[iac2]) ).
fof(iab1,axiom,
incident(ab,a1b1),
file('theBenchmark.p',iab1) ).
cnf(c_53,plain,
incident(ab,a1b1),
inference(clausify,[status(thm)],[iab1]) ).
fof(iab2,axiom,
incident(ab,a2b2),
file('theBenchmark.p',iab2) ).
cnf(c_54,plain,
incident(ab,a2b2),
inference(clausify,[status(thm)],[iab2]) ).
cnf(c_55,plain,
( goal
| ~ incident(c1,A)
| ~ incident(b1,A)
| ~ incident(a1,A) ),
inference(clausify,[status(thm)],[triangle1]) ).
cnf(c_56,plain,
( goal
| ~ incident(c2,A)
| ~ incident(b2,A)
| ~ incident(a2,A) ),
inference(clausify,[status(thm)],[triangle2]) ).
cnf(c_57,plain,
( goal
| ~ point_equal(a2,a1) ),
inference(clausify,[status(thm)],[notaa]) ).
cnf(c_58,plain,
( goal
| ~ point_equal(b2,b1) ),
inference(clausify,[status(thm)],[notbb]) ).
cnf(c_59,plain,
( goal
| ~ point_equal(c2,c1) ),
inference(clausify,[status(thm)],[notcc]) ).
cnf(c_60,plain,
( goal
| ~ line_equal(b1c1,b2c2) ),
inference(clausify,[status(thm)],[notbc]) ).
cnf(c_61,plain,
( goal
| ~ line_equal(a1c1,a2c2) ),
inference(clausify,[status(thm)],[notac]) ).
cnf(c_62,plain,
( goal
| ~ line_equal(a1b1,a2b2) ),
inference(clausify,[status(thm)],[notab]) ).
cnf(c_64,plain,
( point_equal(B,A)
| ~ point_equal(A,B) ),
inference(clausify,[status(thm)],[symmetry_of_point_equal]) ).
cnf(c_65,plain,
( point_equal(A,C)
| ~ point_equal(B,C)
| ~ point_equal(A,B) ),
inference(clausify,[status(thm)],[transitivity_of_point_equal]) ).
cnf(c_66,plain,
( line_equal(B,B)
| ~ incident(A,B) ),
inference(clausify,[status(thm)],[reflexivity_of_line_equal]) ).
cnf(c_67,plain,
( line_equal(B,A)
| ~ line_equal(A,B) ),
inference(clausify,[status(thm)],[symmetry_of_line_equal]) ).
cnf(c_68,plain,
( line_equal(A,C)
| ~ line_equal(B,C)
| ~ line_equal(A,B) ),
inference(clausify,[status(thm)],[transitivity_of_line_equal]) ).
cnf(c_69,plain,
( incident(A,C)
| ~ incident(B,C)
| ~ point_equal(A,B) ),
inference(clausify,[status(thm)],[pcon]) ).
cnf(c_70,plain,
( incident(A,C)
| ~ line_equal(B,C)
| ~ incident(A,B) ),
inference(clausify,[status(thm)],[lcon]) ).
cnf(c_71,plain,
( line_equal(B,C)
| point_equal(A,D)
| ~ incident(D,C)
| ~ incident(D,B)
| ~ incident(A,C)
| ~ incident(A,B) ),
inference(clausify,[status(thm)],[unique]) ).
cnf(c_72,negated_conjecture,
~ goal,
inference(clausify,[status(thm)],[goal_to_be_proved_neg]) ).
cnf(c_73,negated_conjecture,
~ line_equal(a1b1,a2b2),
inference(resolve,[status(thm)],[c_72,c_62]) ).
cnf(c_74,negated_conjecture,
~ line_equal(a1c1,a2c2),
inference(resolve,[status(thm)],[c_72,c_61]) ).
cnf(c_75,negated_conjecture,
~ line_equal(b1c1,b2c2),
inference(resolve,[status(thm)],[c_72,c_60]) ).
cnf(c_76,negated_conjecture,
~ point_equal(c2,c1),
inference(resolve,[status(thm)],[c_72,c_59]) ).
cnf(c_77,negated_conjecture,
~ point_equal(b2,b1),
inference(resolve,[status(thm)],[c_72,c_58]) ).
cnf(c_78,negated_conjecture,
~ point_equal(a2,a1),
inference(resolve,[status(thm)],[c_72,c_57]) ).
cnf(c_79,negated_conjecture,
( ~ incident(c2,A)
| ~ incident(b2,A)
| ~ incident(a2,A) ),
inference(resolve,[status(thm)],[c_72,c_56]) ).
cnf(c_80,negated_conjecture,
( ~ incident(c1,A)
| ~ incident(b1,A)
| ~ incident(a1,A) ),
inference(resolve,[status(thm)],[c_72,c_55]) ).
cnf(c_81,negated_conjecture,
( ~ incident(c2,a1b1)
| ~ incident(b2,a1c1)
| ~ incident(a2,b1c1) ),
inference(resolve,[status(thm)],[c_72,c_24]) ).
cnf(c_82,negated_conjecture,
( ~ incident(c1,a2b2)
| ~ incident(b1,a2c2)
| ~ incident(a1,b2c2) ),
inference(resolve,[status(thm)],[c_72,c_23]) ).
cnf(c_83,negated_conjecture,
( ~ incident(ab,A)
| ~ incident(ac,A)
| ~ incident(bc,A)
| ~ line_equal(A,A) ),
inference(resolve,[status(thm)],[c_72,c_22]) ).
cnf(c_94,plain,
line_equal(a2b2,a2b2),
inference(resolve,[status(thm)],[c_66,c_54]) ).
cnf(c_96,plain,
line_equal(a2c2,a2c2),
inference(resolve,[status(thm)],[c_66,c_52]) ).
cnf(c_98,plain,
line_equal(b2c2,b2c2),
inference(resolve,[status(thm)],[c_66,c_50]) ).
cnf(c_103,plain,
( line_equal(a2b2,A)
| point_equal(ab,B)
| ~ incident(B,A)
| ~ incident(B,a2b2)
| ~ incident(ab,A) ),
inference(resolve,[status(thm)],[c_71,c_54]) ).
cnf(c_106,plain,
( line_equal(a1c1,A)
| point_equal(ac,B)
| ~ incident(B,A)
| ~ incident(B,a1c1)
| ~ incident(ac,A) ),
inference(resolve,[status(thm)],[c_71,c_51]) ).
cnf(c_108,plain,
( line_equal(b1c1,A)
| point_equal(bc,B)
| ~ incident(B,A)
| ~ incident(B,b1c1)
| ~ incident(bc,A) ),
inference(resolve,[status(thm)],[c_71,c_49]) ).
cnf(c_109,plain,
( line_equal(oc,A)
| point_equal(c2,B)
| ~ incident(B,A)
| ~ incident(B,oc)
| ~ incident(c2,A) ),
inference(resolve,[status(thm)],[c_71,c_48]) ).
cnf(c_110,plain,
( line_equal(oc,A)
| point_equal(c1,B)
| ~ incident(B,A)
| ~ incident(B,oc)
| ~ incident(c1,A) ),
inference(resolve,[status(thm)],[c_71,c_47]) ).
cnf(c_112,plain,
( line_equal(ob,A)
| point_equal(b1,B)
| ~ incident(B,A)
| ~ incident(B,ob)
| ~ incident(b1,A) ),
inference(resolve,[status(thm)],[c_71,c_45]) ).
cnf(c_113,plain,
( line_equal(oa,A)
| point_equal(a2,B)
| ~ incident(B,A)
| ~ incident(B,oa)
| ~ incident(a2,A) ),
inference(resolve,[status(thm)],[c_71,c_44]) ).
cnf(c_119,plain,
( line_equal(b2c2,A)
| point_equal(c2,B)
| ~ incident(B,A)
| ~ incident(B,b2c2)
| ~ incident(c2,A) ),
inference(resolve,[status(thm)],[c_71,c_38]) ).
cnf(c_121,plain,
( line_equal(b1c1,A)
| point_equal(c1,B)
| ~ incident(B,A)
| ~ incident(B,b1c1)
| ~ incident(c1,A) ),
inference(resolve,[status(thm)],[c_71,c_36]) ).
cnf(c_122,plain,
( line_equal(a2c2,A)
| point_equal(c2,B)
| ~ incident(B,A)
| ~ incident(B,a2c2)
| ~ incident(c2,A) ),
inference(resolve,[status(thm)],[c_71,c_35]) ).
cnf(c_127,plain,
( line_equal(a2b2,A)
| point_equal(a2,B)
| ~ incident(B,A)
| ~ incident(B,a2b2)
| ~ incident(a2,A) ),
inference(resolve,[status(thm)],[c_71,c_30]) ).
cnf(c_130,plain,
( incident(a2,b1c1)
| line_equal(a2b2,A)
| point_equal(c1,B)
| ~ incident(B,A)
| ~ incident(B,a2b2)
| ~ incident(c1,A) ),
inference(resolve,[status(thm)],[c_71,c_27]) ).
cnf(c_131,plain,
( incident(b1,a2c2)
| line_equal(a1b1,A)
| point_equal(c2,B)
| ~ incident(B,A)
| ~ incident(B,a1b1)
| ~ incident(c2,A) ),
inference(resolve,[status(thm)],[c_71,c_26]) ).
cnf(c_137,plain,
( line_equal(A,b2c2)
| point_equal(bc,B)
| ~ incident(B,b2c2)
| ~ incident(B,A)
| ~ incident(bc,A) ),
inference(resolve,[status(thm)],[c_71,c_50]) ).
cnf(c_140,plain,
( line_equal(A,oc)
| point_equal(c1,B)
| ~ incident(B,oc)
| ~ incident(B,A)
| ~ incident(c1,A) ),
inference(resolve,[status(thm)],[c_71,c_47]) ).
cnf(c_142,plain,
( line_equal(A,ob)
| point_equal(b1,B)
| ~ incident(B,ob)
| ~ incident(B,A)
| ~ incident(b1,A) ),
inference(resolve,[status(thm)],[c_71,c_45]) ).
cnf(c_143,plain,
( line_equal(A,oa)
| point_equal(a2,B)
| ~ incident(B,oa)
| ~ incident(B,A)
| ~ incident(a2,A) ),
inference(resolve,[status(thm)],[c_71,c_44]) ).
cnf(c_153,plain,
( line_equal(A,a2c2)
| point_equal(a2,B)
| ~ incident(B,a2c2)
| ~ incident(B,A)
| ~ incident(a2,A) ),
inference(resolve,[status(thm)],[c_71,c_34]) ).
cnf(c_156,plain,
( line_equal(A,a2b2)
| point_equal(b2,B)
| ~ incident(B,a2b2)
| ~ incident(B,A)
| ~ incident(b2,A) ),
inference(resolve,[status(thm)],[c_71,c_31]) ).
cnf(c_159,plain,
( line_equal(A,a1b1)
| point_equal(a1,B)
| ~ incident(B,a1b1)
| ~ incident(B,A)
| ~ incident(a1,A) ),
inference(resolve,[status(thm)],[c_71,c_28]) ).
cnf(c_163,plain,
( line_equal(a2b2,B)
| point_equal(A,ab)
| ~ incident(ab,B)
| ~ incident(A,B)
| ~ incident(A,a2b2) ),
inference(resolve,[status(thm)],[c_71,c_54]) ).
cnf(c_165,plain,
( line_equal(a2c2,B)
| point_equal(A,ac)
| ~ incident(ac,B)
| ~ incident(A,B)
| ~ incident(A,a2c2) ),
inference(resolve,[status(thm)],[c_71,c_52]) ).
cnf(c_169,plain,
( line_equal(oc,B)
| point_equal(A,c2)
| ~ incident(c2,B)
| ~ incident(A,B)
| ~ incident(A,oc) ),
inference(resolve,[status(thm)],[c_71,c_48]) ).
cnf(c_171,plain,
( line_equal(ob,B)
| point_equal(A,b2)
| ~ incident(b2,B)
| ~ incident(A,B)
| ~ incident(A,ob) ),
inference(resolve,[status(thm)],[c_71,c_46]) ).
cnf(c_172,plain,
( line_equal(ob,B)
| point_equal(A,b1)
| ~ incident(b1,B)
| ~ incident(A,B)
| ~ incident(A,ob) ),
inference(resolve,[status(thm)],[c_71,c_45]) ).
cnf(c_173,plain,
( line_equal(oa,B)
| point_equal(A,a2)
| ~ incident(a2,B)
| ~ incident(A,B)
| ~ incident(A,oa) ),
inference(resolve,[status(thm)],[c_71,c_44]) ).
cnf(c_174,plain,
( line_equal(oa,B)
| point_equal(A,a1)
| ~ incident(a1,B)
| ~ incident(A,B)
| ~ incident(A,oa) ),
inference(resolve,[status(thm)],[c_71,c_43]) ).
cnf(c_178,plain,
( line_equal(b2c2,B)
| point_equal(A,b2)
| ~ incident(b2,B)
| ~ incident(A,B)
| ~ incident(A,b2c2) ),
inference(resolve,[status(thm)],[c_71,c_39]) ).
cnf(c_185,plain,
( line_equal(a1c1,B)
| point_equal(A,a1)
| ~ incident(a1,B)
| ~ incident(A,B)
| ~ incident(A,a1c1) ),
inference(resolve,[status(thm)],[c_71,c_32]) ).
cnf(c_187,plain,
( line_equal(a2b2,B)
| point_equal(A,a2)
| ~ incident(a2,B)
| ~ incident(A,B)
| ~ incident(A,a2b2) ),
inference(resolve,[status(thm)],[c_71,c_30]) ).
cnf(c_188,plain,
( line_equal(a1b1,B)
| point_equal(A,b1)
| ~ incident(b1,B)
| ~ incident(A,B)
| ~ incident(A,a1b1) ),
inference(resolve,[status(thm)],[c_71,c_29]) ).
cnf(c_200,plain,
( line_equal(B,oc)
| point_equal(A,c1)
| ~ incident(c1,B)
| ~ incident(A,oc)
| ~ incident(A,B) ),
inference(resolve,[status(thm)],[c_71,c_47]) ).
cnf(c_202,plain,
( line_equal(B,ob)
| point_equal(A,b1)
| ~ incident(b1,B)
| ~ incident(A,ob)
| ~ incident(A,B) ),
inference(resolve,[status(thm)],[c_71,c_45]) ).
cnf(c_204,plain,
( line_equal(B,oa)
| point_equal(A,a1)
| ~ incident(a1,B)
| ~ incident(A,oa)
| ~ incident(A,B) ),
inference(resolve,[status(thm)],[c_71,c_43]) ).
cnf(c_207,plain,
( line_equal(B,oa)
| point_equal(A,o)
| ~ incident(o,B)
| ~ incident(A,oa)
| ~ incident(A,B) ),
inference(resolve,[status(thm)],[c_71,c_40]) ).
cnf(c_223,plain,
~ line_equal(a2b2,a1b1),
inference(resolve,[status(thm)],[c_67,c_73]) ).
cnf(c_224,plain,
~ line_equal(a2c2,a1c1),
inference(resolve,[status(thm)],[c_67,c_74]) ).
cnf(c_226,plain,
~ point_equal(c1,c2),
inference(resolve,[status(thm)],[c_64,c_76]) ).
cnf(c_228,plain,
~ point_equal(a1,a2),
inference(resolve,[status(thm)],[c_64,c_78]) ).
cnf(c_10793,plain,
( ~ incident(b2,b2c2)
| ~ incident(a2,b2c2) ),
inference(resolve,[status(thm)],[c_79,c_38]) ).
cnf(c_230,plain,
~ incident(a2,b2c2),
inference(resolve,[status(thm)],[c_39,c_10793]) ).
cnf(c_10794,plain,
( ~ incident(b2,a2c2)
| ~ incident(a2,a2c2) ),
inference(resolve,[status(thm)],[c_79,c_35]) ).
cnf(c_231,plain,
~ incident(b2,a2c2),
inference(resolve,[status(thm)],[c_34,c_10794]) ).
cnf(c_10795,plain,
( ~ incident(c2,a2b2)
| ~ incident(b2,a2b2) ),
inference(resolve,[status(thm)],[c_79,c_30]) ).
cnf(c_233,plain,
~ incident(c2,a2b2),
inference(resolve,[status(thm)],[c_10795,c_31]) ).
cnf(c_10796,plain,
( ~ incident(b1,b1c1)
| ~ incident(a1,b1c1) ),
inference(resolve,[status(thm)],[c_80,c_36]) ).
cnf(c_235,plain,
~ incident(a1,b1c1),
inference(resolve,[status(thm)],[c_37,c_10796]) ).
cnf(c_10797,plain,
( ~ incident(b1,a1c1)
| ~ incident(a1,a1c1) ),
inference(resolve,[status(thm)],[c_80,c_33]) ).
cnf(c_236,plain,
~ incident(b1,a1c1),
inference(resolve,[status(thm)],[c_32,c_10797]) ).
cnf(c_10798,plain,
( ~ incident(c1,a1b1)
| ~ incident(b1,a1b1) ),
inference(resolve,[status(thm)],[c_80,c_28]) ).
cnf(c_238,plain,
~ incident(c1,a1b1),
inference(resolve,[status(thm)],[c_10798,c_29]) ).
cnf(c_239,plain,
( incident(b1,a2c2)
| ~ incident(b2,a1c1)
| ~ incident(a2,b1c1) ),
inference(resolve,[status(thm)],[c_81,c_26]) ).
cnf(c_240,plain,
( incident(a2,b1c1)
| ~ incident(b1,a2c2)
| ~ incident(a1,b2c2) ),
inference(resolve,[status(thm)],[c_82,c_27]) ).
cnf(c_10799,plain,
( incident(a2,A)
| ~ line_equal(oa,A) ),
inference(resolve,[status(thm)],[c_70,c_44]) ).
cnf(c_241,plain,
~ line_equal(oa,b2c2),
inference(resolve,[status(thm)],[c_10799,c_230]) ).
cnf(c_10800,plain,
( incident(A,b2c2)
| ~ point_equal(A,bc) ),
inference(resolve,[status(thm)],[c_69,c_50]) ).
cnf(c_244,plain,
~ point_equal(a2,bc),
inference(resolve,[status(thm)],[c_10800,c_230]) ).
cnf(c_10801,plain,
( incident(A,b2c2)
| ~ point_equal(A,b2) ),
inference(resolve,[status(thm)],[c_69,c_39]) ).
cnf(c_245,plain,
~ point_equal(a2,b2),
inference(resolve,[status(thm)],[c_10801,c_230]) ).
cnf(c_10802,plain,
( incident(b2,A)
| ~ line_equal(ob,A) ),
inference(resolve,[status(thm)],[c_70,c_46]) ).
cnf(c_247,plain,
~ line_equal(ob,a2c2),
inference(resolve,[status(thm)],[c_10802,c_231]) ).
cnf(c_10803,plain,
( incident(A,a2c2)
| ~ point_equal(A,ac) ),
inference(resolve,[status(thm)],[c_69,c_52]) ).
cnf(c_250,plain,
~ point_equal(b2,ac),
inference(resolve,[status(thm)],[c_10803,c_231]) ).
cnf(c_10804,plain,
( ~ incident(ab,a2b2)
| ~ incident(ac,a2b2)
| ~ incident(bc,a2b2) ),
inference(resolve,[status(thm)],[c_94,c_83]) ).
cnf(c_253,plain,
( ~ incident(ac,a2b2)
| ~ incident(bc,a2b2) ),
inference(resolve,[status(thm)],[c_54,c_10804]) ).
cnf(c_10805,plain,
( incident(c2,A)
| ~ line_equal(oc,A) ),
inference(resolve,[status(thm)],[c_70,c_48]) ).
cnf(c_254,plain,
~ line_equal(oc,a2b2),
inference(resolve,[status(thm)],[c_10805,c_233]) ).
cnf(c_10806,plain,
( incident(c2,A)
| ~ line_equal(b2c2,A) ),
inference(resolve,[status(thm)],[c_70,c_38]) ).
cnf(c_255,plain,
~ line_equal(b2c2,a2b2),
inference(resolve,[status(thm)],[c_10806,c_233]) ).
cnf(c_10807,plain,
( incident(A,a2b2)
| ~ point_equal(A,ab) ),
inference(resolve,[status(thm)],[c_69,c_54]) ).
cnf(c_257,plain,
~ point_equal(c2,ab),
inference(resolve,[status(thm)],[c_10807,c_233]) ).
cnf(c_10808,plain,
( incident(A,a2b2)
| ~ point_equal(A,a2) ),
inference(resolve,[status(thm)],[c_69,c_30]) ).
cnf(c_259,plain,
~ point_equal(c2,a2),
inference(resolve,[status(thm)],[c_10808,c_233]) ).
cnf(c_10809,plain,
( incident(a1,A)
| ~ line_equal(oa,A) ),
inference(resolve,[status(thm)],[c_70,c_43]) ).
cnf(c_260,plain,
~ line_equal(oa,b1c1),
inference(resolve,[status(thm)],[c_10809,c_235]) ).
cnf(c_10810,plain,
( incident(A,b1c1)
| ~ point_equal(A,bc) ),
inference(resolve,[status(thm)],[c_69,c_49]) ).
cnf(c_263,plain,
~ point_equal(a1,bc),
inference(resolve,[status(thm)],[c_10810,c_235]) ).
cnf(c_10811,plain,
( incident(b1,A)
| ~ line_equal(ob,A) ),
inference(resolve,[status(thm)],[c_70,c_45]) ).
cnf(c_266,plain,
~ line_equal(ob,a1c1),
inference(resolve,[status(thm)],[c_10811,c_236]) ).
cnf(c_10812,plain,
( incident(A,a1c1)
| ~ point_equal(A,ac) ),
inference(resolve,[status(thm)],[c_69,c_51]) ).
cnf(c_269,plain,
~ point_equal(b1,ac),
inference(resolve,[status(thm)],[c_10812,c_236]) ).
cnf(c_10813,plain,
( incident(A,a1c1)
| ~ point_equal(A,a1) ),
inference(resolve,[status(thm)],[c_69,c_32]) ).
cnf(c_271,plain,
~ point_equal(b1,a1),
inference(resolve,[status(thm)],[c_10813,c_236]) ).
cnf(c_10814,plain,
( incident(c1,A)
| ~ line_equal(oc,A) ),
inference(resolve,[status(thm)],[c_70,c_47]) ).
cnf(c_272,plain,
~ line_equal(oc,a1b1),
inference(resolve,[status(thm)],[c_10814,c_238]) ).
cnf(c_10815,plain,
( incident(c1,A)
| ~ line_equal(a1c1,A) ),
inference(resolve,[status(thm)],[c_70,c_33]) ).
cnf(c_274,plain,
~ line_equal(a1c1,a1b1),
inference(resolve,[status(thm)],[c_10815,c_238]) ).
cnf(c_10816,plain,
( incident(A,a1b1)
| ~ point_equal(A,ab) ),
inference(resolve,[status(thm)],[c_69,c_53]) ).
cnf(c_275,plain,
~ point_equal(c1,ab),
inference(resolve,[status(thm)],[c_10816,c_238]) ).
cnf(c_10817,plain,
( incident(A,a1b1)
| ~ point_equal(A,b1) ),
inference(resolve,[status(thm)],[c_69,c_29]) ).
cnf(c_276,plain,
~ point_equal(c1,b1),
inference(resolve,[status(thm)],[c_10817,c_238]) ).
cnf(c_10818,plain,
( ~ incident(ab,a2c2)
| ~ incident(ac,a2c2)
| ~ incident(bc,a2c2) ),
inference(resolve,[status(thm)],[c_96,c_83]) ).
cnf(c_279,plain,
( ~ incident(ab,a2c2)
| ~ incident(bc,a2c2) ),
inference(resolve,[status(thm)],[c_52,c_10818]) ).
cnf(c_10819,plain,
( ~ incident(ab,b2c2)
| ~ incident(ac,b2c2)
| ~ incident(bc,b2c2) ),
inference(resolve,[status(thm)],[c_98,c_83]) ).
cnf(c_281,plain,
( ~ incident(ab,b2c2)
| ~ incident(ac,b2c2) ),
inference(resolve,[status(thm)],[c_50,c_10819]) ).
cnf(c_283,plain,
~ line_equal(b2c2,oa),
inference(resolve,[status(thm)],[c_67,c_241]) ).
cnf(c_284,plain,
~ point_equal(bc,a2),
inference(resolve,[status(thm)],[c_64,c_244]) ).
cnf(c_10820,plain,
( line_equal(a2b2,a1b1)
| point_equal(ab,b1)
| ~ incident(b1,a2b2)
| ~ incident(ab,a1b1) ),
inference(resolve,[status(thm)],[c_103,c_29]) ).
cnf(c_10821,plain,
( line_equal(a2b2,a1b1)
| point_equal(ab,b1)
| ~ incident(b1,a2b2) ),
inference(resolve,[status(thm)],[c_53,c_10820]) ).
cnf(c_310,plain,
( point_equal(ab,b1)
| ~ incident(b1,a2b2) ),
inference(resolve,[status(thm)],[c_223,c_10821]) ).
cnf(c_313,plain,
~ line_equal(a2c2,ob),
inference(resolve,[status(thm)],[c_67,c_247]) ).
cnf(c_335,plain,
~ point_equal(ac,b2),
inference(resolve,[status(thm)],[c_64,c_250]) ).
cnf(c_359,plain,
~ line_equal(a2b2,oc),
inference(resolve,[status(thm)],[c_67,c_254]) ).
cnf(c_362,plain,
~ point_equal(ab,c2),
inference(resolve,[status(thm)],[c_64,c_257]) ).
cnf(c_10822,plain,
( line_equal(a1c1,a2c2)
| point_equal(ac,c2)
| ~ incident(c2,a1c1)
| ~ incident(ac,a2c2) ),
inference(resolve,[status(thm)],[c_106,c_35]) ).
cnf(c_10823,plain,
( line_equal(a1c1,a2c2)
| point_equal(ac,c2)
| ~ incident(c2,a1c1) ),
inference(resolve,[status(thm)],[c_52,c_10822]) ).
cnf(c_384,plain,
( point_equal(ac,c2)
| ~ incident(c2,a1c1) ),
inference(resolve,[status(thm)],[c_74,c_10823]) ).
cnf(c_389,plain,
~ line_equal(b1c1,oa),
inference(resolve,[status(thm)],[c_67,c_260]) ).
cnf(c_413,plain,
~ point_equal(bc,a1),
inference(resolve,[status(thm)],[c_64,c_263]) ).
cnf(c_10824,plain,
( line_equal(b1c1,b2c2)
| point_equal(bc,b2)
| ~ incident(b2,b1c1)
| ~ incident(bc,b2c2) ),
inference(resolve,[status(thm)],[c_108,c_39]) ).
cnf(c_10825,plain,
( line_equal(b1c1,b2c2)
| point_equal(bc,b2)
| ~ incident(b2,b1c1) ),
inference(resolve,[status(thm)],[c_50,c_10824]) ).
cnf(c_431,plain,
( point_equal(bc,b2)
| ~ incident(b2,b1c1) ),
inference(resolve,[status(thm)],[c_75,c_10825]) ).
cnf(c_441,plain,
~ point_equal(ac,b1),
inference(resolve,[status(thm)],[c_64,c_269]) ).
cnf(c_10826,plain,
( line_equal(oc,a2c2)
| point_equal(c2,a2)
| ~ incident(a2,oc)
| ~ incident(c2,a2c2) ),
inference(resolve,[status(thm)],[c_109,c_34]) ).
cnf(c_10827,plain,
( line_equal(oc,a2c2)
| point_equal(c2,a2)
| ~ incident(a2,oc) ),
inference(resolve,[status(thm)],[c_35,c_10826]) ).
cnf(c_464,plain,
( line_equal(oc,a2c2)
| ~ incident(a2,oc) ),
inference(resolve,[status(thm)],[c_259,c_10827]) ).
cnf(c_10828,plain,
( line_equal(oc,a1c1)
| point_equal(c2,c1)
| ~ incident(c1,oc)
| ~ incident(c2,a1c1) ),
inference(resolve,[status(thm)],[c_109,c_33]) ).
cnf(c_10829,plain,
( line_equal(oc,a1c1)
| point_equal(c2,c1)
| ~ incident(c2,a1c1) ),
inference(resolve,[status(thm)],[c_47,c_10828]) ).
cnf(c_465,plain,
( line_equal(oc,a1c1)
| ~ incident(c2,a1c1) ),
inference(resolve,[status(thm)],[c_76,c_10829]) ).
cnf(c_468,plain,
~ line_equal(a1b1,oc),
inference(resolve,[status(thm)],[c_67,c_272]) ).
cnf(c_10830,plain,
( line_equal(oc,b2c2)
| point_equal(c1,c2)
| ~ incident(c2,oc)
| ~ incident(c1,b2c2) ),
inference(resolve,[status(thm)],[c_110,c_38]) ).
cnf(c_10831,plain,
( line_equal(oc,b2c2)
| point_equal(c1,c2)
| ~ incident(c1,b2c2) ),
inference(resolve,[status(thm)],[c_48,c_10830]) ).
cnf(c_485,plain,
( line_equal(oc,b2c2)
| ~ incident(c1,b2c2) ),
inference(resolve,[status(thm)],[c_226,c_10831]) ).
cnf(c_10832,plain,
( line_equal(oc,a2c2)
| point_equal(c1,c2)
| ~ incident(c2,oc)
| ~ incident(c1,a2c2) ),
inference(resolve,[status(thm)],[c_110,c_35]) ).
cnf(c_10833,plain,
( line_equal(oc,a2c2)
| point_equal(c1,c2)
| ~ incident(c1,a2c2) ),
inference(resolve,[status(thm)],[c_48,c_10832]) ).
cnf(c_487,plain,
( line_equal(oc,a2c2)
| ~ incident(c1,a2c2) ),
inference(resolve,[status(thm)],[c_226,c_10833]) ).
cnf(c_492,plain,
~ point_equal(ab,c1),
inference(resolve,[status(thm)],[c_64,c_275]) ).
cnf(c_10834,plain,
( line_equal(ob,a2c2)
| point_equal(b1,a2)
| ~ incident(a2,ob)
| ~ incident(b1,a2c2) ),
inference(resolve,[status(thm)],[c_112,c_34]) ).
cnf(c_534,plain,
( point_equal(b1,a2)
| ~ incident(a2,ob)
| ~ incident(b1,a2c2) ),
inference(resolve,[status(thm)],[c_247,c_10834]) ).
cnf(c_10835,plain,
( line_equal(ob,a1b1)
| point_equal(b1,a1)
| ~ incident(a1,ob)
| ~ incident(b1,a1b1) ),
inference(resolve,[status(thm)],[c_112,c_28]) ).
cnf(c_10836,plain,
( line_equal(ob,a1b1)
| point_equal(b1,a1)
| ~ incident(a1,ob) ),
inference(resolve,[status(thm)],[c_29,c_10835]) ).
cnf(c_536,plain,
( line_equal(ob,a1b1)
| ~ incident(a1,ob) ),
inference(resolve,[status(thm)],[c_271,c_10836]) ).
cnf(c_10837,plain,
( line_equal(oa,ob)
| point_equal(a2,o)
| ~ incident(o,oa)
| ~ incident(a2,ob) ),
inference(resolve,[status(thm)],[c_113,c_41]) ).
cnf(c_551,plain,
( line_equal(oa,ob)
| point_equal(a2,o)
| ~ incident(a2,ob) ),
inference(resolve,[status(thm)],[c_40,c_10837]) ).
cnf(c_607,plain,
( incident(a1,b2c2)
| incident(b1,a2c2)
| ~ incident(a2,b1c1) ),
inference(resolve,[status(thm)],[c_239,c_25]) ).
cnf(c_10838,plain,
( line_equal(b1c1,oa)
| point_equal(c1,a2)
| ~ incident(a2,b1c1)
| ~ incident(c1,oa) ),
inference(resolve,[status(thm)],[c_121,c_44]) ).
cnf(c_724,plain,
( point_equal(c1,a2)
| ~ incident(a2,b1c1)
| ~ incident(c1,oa) ),
inference(resolve,[status(thm)],[c_389,c_10838]) ).
cnf(c_10839,plain,
( line_equal(a2c2,oc)
| point_equal(c2,c1)
| ~ incident(c1,a2c2)
| ~ incident(c2,oc) ),
inference(resolve,[status(thm)],[c_122,c_47]) ).
cnf(c_10840,plain,
( line_equal(a2c2,oc)
| point_equal(c2,c1)
| ~ incident(c1,a2c2) ),
inference(resolve,[status(thm)],[c_48,c_10839]) ).
cnf(c_740,plain,
( line_equal(a2c2,oc)
| ~ incident(c1,a2c2) ),
inference(resolve,[status(thm)],[c_76,c_10840]) ).
cnf(c_10841,plain,
( line_equal(a2b2,ob)
| point_equal(a2,b2)
| ~ incident(b2,a2b2)
| ~ incident(a2,ob) ),
inference(resolve,[status(thm)],[c_127,c_46]) ).
cnf(c_10842,plain,
( line_equal(a2b2,ob)
| point_equal(a2,b2)
| ~ incident(a2,ob) ),
inference(resolve,[status(thm)],[c_31,c_10841]) ).
cnf(c_835,plain,
( line_equal(a2b2,ob)
| ~ incident(a2,ob) ),
inference(resolve,[status(thm)],[c_245,c_10842]) ).
cnf(c_10843,plain,
( incident(a2,b1c1)
| line_equal(a2b2,oc)
| point_equal(c1,o)
| ~ incident(o,a2b2)
| ~ incident(c1,oc) ),
inference(resolve,[status(thm)],[c_130,c_42]) ).
cnf(c_10844,plain,
( incident(a2,b1c1)
| line_equal(a2b2,oc)
| point_equal(c1,o)
| ~ incident(o,a2b2) ),
inference(resolve,[status(thm)],[c_47,c_10843]) ).
cnf(c_889,plain,
( incident(a2,b1c1)
| point_equal(c1,o)
| ~ incident(o,a2b2) ),
inference(resolve,[status(thm)],[c_359,c_10844]) ).
cnf(c_10845,plain,
( incident(a1,b2c2)
| incident(a2,b1c1)
| line_equal(a2b2,a1c1)
| point_equal(c1,b2)
| ~ incident(b2,a2b2)
| ~ incident(c1,a1c1) ),
inference(resolve,[status(thm)],[c_130,c_25]) ).
cnf(c_10846,plain,
( incident(a1,b2c2)
| incident(a2,b1c1)
| line_equal(a2b2,a1c1)
| point_equal(c1,b2)
| ~ incident(b2,a2b2) ),
inference(resolve,[status(thm)],[c_33,c_10845]) ).
cnf(c_894,plain,
( incident(a1,b2c2)
| incident(a2,b1c1)
| line_equal(a2b2,a1c1)
| point_equal(c1,b2) ),
inference(resolve,[status(thm)],[c_31,c_10846]) ).
cnf(c_898,plain,
( incident(b1,a2c2)
| line_equal(a1b1,A)
| point_equal(c2,a1)
| ~ incident(a1,A)
| ~ incident(c2,A) ),
inference(resolve,[status(thm)],[c_131,c_28]) ).
cnf(c_10847,plain,
( incident(b1,a2c2)
| line_equal(a1b1,oc)
| point_equal(c2,o)
| ~ incident(o,a1b1)
| ~ incident(c2,oc) ),
inference(resolve,[status(thm)],[c_131,c_42]) ).
cnf(c_10848,plain,
( incident(b1,a2c2)
| line_equal(a1b1,oc)
| point_equal(c2,o)
| ~ incident(o,a1b1) ),
inference(resolve,[status(thm)],[c_48,c_10847]) ).
cnf(c_903,plain,
( incident(b1,a2c2)
| point_equal(c2,o)
| ~ incident(o,a1b1) ),
inference(resolve,[status(thm)],[c_468,c_10848]) ).
cnf(c_10849,plain,
( line_equal(oc,oa)
| point_equal(a2,o)
| ~ incident(o,oa)
| ~ incident(a2,oc) ),
inference(resolve,[status(thm)],[c_143,c_42]) ).
cnf(c_1022,plain,
( line_equal(oc,oa)
| point_equal(a2,o)
| ~ incident(a2,oc) ),
inference(resolve,[status(thm)],[c_40,c_10849]) ).
cnf(c_1108,plain,
( line_equal(b1c1,a2c2)
| point_equal(a2,b1)
| ~ incident(b1,a2c2)
| ~ incident(a2,b1c1) ),
inference(resolve,[status(thm)],[c_153,c_37]) ).
cnf(c_1129,plain,
( line_equal(A,a2b2)
| point_equal(b2,ab)
| ~ incident(ab,A)
| ~ incident(b2,A) ),
inference(resolve,[status(thm)],[c_156,c_54]) ).
cnf(c_1149,plain,
( line_equal(A,a1b1)
| point_equal(a1,ab)
| ~ incident(ab,A)
| ~ incident(a1,A) ),
inference(resolve,[status(thm)],[c_159,c_53]) ).
cnf(c_10850,plain,
( line_equal(a2b2,a1b1)
| point_equal(A,ab)
| ~ incident(A,a1b1)
| ~ incident(A,a2b2) ),
inference(resolve,[status(thm)],[c_163,c_53]) ).
cnf(c_1171,plain,
( point_equal(A,ab)
| ~ incident(A,a1b1)
| ~ incident(A,a2b2) ),
inference(resolve,[status(thm)],[c_223,c_10850]) ).
cnf(c_10851,plain,
( line_equal(a2c2,a1c1)
| point_equal(A,ac)
| ~ incident(A,a1c1)
| ~ incident(A,a2c2) ),
inference(resolve,[status(thm)],[c_165,c_51]) ).
cnf(c_1172,plain,
( point_equal(A,ac)
| ~ incident(A,a1c1)
| ~ incident(A,a2c2) ),
inference(resolve,[status(thm)],[c_224,c_10851]) ).
cnf(c_1181,plain,
( line_equal(ob,a2b2)
| point_equal(A,b2)
| ~ incident(A,a2b2)
| ~ incident(A,ob) ),
inference(resolve,[status(thm)],[c_171,c_31]) ).
cnf(c_10852,plain,
( incident(a1,b2c2)
| line_equal(ob,a1c1)
| point_equal(A,b2)
| ~ incident(A,a1c1)
| ~ incident(A,ob) ),
inference(resolve,[status(thm)],[c_171,c_25]) ).
cnf(c_1182,plain,
( incident(a1,b2c2)
| point_equal(A,b2)
| ~ incident(A,a1c1)
| ~ incident(A,ob) ),
inference(resolve,[status(thm)],[c_266,c_10852]) ).
cnf(c_1183,plain,
( line_equal(ob,b1c1)
| point_equal(A,b1)
| ~ incident(A,b1c1)
| ~ incident(A,ob) ),
inference(resolve,[status(thm)],[c_172,c_37]) ).
cnf(c_1185,plain,
( line_equal(oa,a2c2)
| point_equal(A,a2)
| ~ incident(A,a2c2)
| ~ incident(A,oa) ),
inference(resolve,[status(thm)],[c_173,c_34]) ).
cnf(c_1188,plain,
( line_equal(oa,a1b1)
| point_equal(A,a1)
| ~ incident(A,a1b1)
| ~ incident(A,oa) ),
inference(resolve,[status(thm)],[c_174,c_28]) ).
cnf(c_10853,plain,
( line_equal(b2c2,a2b2)
| point_equal(A,b2)
| ~ incident(A,a2b2)
| ~ incident(A,b2c2) ),
inference(resolve,[status(thm)],[c_178,c_31]) ).
cnf(c_1196,plain,
( point_equal(A,b2)
| ~ incident(A,a2b2)
| ~ incident(A,b2c2) ),
inference(resolve,[status(thm)],[c_255,c_10853]) ).
cnf(c_10854,plain,
( line_equal(a1c1,a1b1)
| point_equal(A,a1)
| ~ incident(A,a1b1)
| ~ incident(A,a1c1) ),
inference(resolve,[status(thm)],[c_185,c_28]) ).
cnf(c_1217,plain,
( point_equal(A,a1)
| ~ incident(A,a1b1)
| ~ incident(A,a1c1) ),
inference(resolve,[status(thm)],[c_274,c_10854]) ).
cnf(c_1221,plain,
( line_equal(a2b2,oa)
| point_equal(A,a2)
| ~ incident(A,oa)
| ~ incident(A,a2b2) ),
inference(resolve,[status(thm)],[c_187,c_44]) ).
cnf(c_1222,plain,
( line_equal(a1b1,ob)
| point_equal(A,b1)
| ~ incident(A,ob)
| ~ incident(A,a1b1) ),
inference(resolve,[status(thm)],[c_188,c_45]) ).
cnf(c_1245,plain,
( incident(c1,A)
| ~ incident(b2,A)
| incident(a1,b2c2)
| incident(a2,b1c1)
| line_equal(a2b2,a1c1) ),
inference(resolve,[status(thm)],[c_894,c_69]) ).
cnf(c_1256,plain,
( incident(b1,a2c2)
| line_equal(a1b1,b2c2)
| point_equal(c2,a1)
| ~ incident(a1,b2c2) ),
inference(resolve,[status(thm)],[c_898,c_38]) ).
cnf(c_1272,plain,
( incident(c1,ob)
| incident(a1,b2c2)
| incident(a2,b1c1)
| line_equal(a2b2,a1c1) ),
inference(resolve,[status(thm)],[c_1245,c_46]) ).
cnf(c_1274,plain,
( incident(A,a1c1)
| ~ incident(A,a2b2)
| incident(c1,ob)
| incident(a1,b2c2)
| incident(a2,b1c1) ),
inference(resolve,[status(thm)],[c_1272,c_70]) ).
cnf(c_1304,plain,
( incident(ab,a1c1)
| incident(c1,ob)
| incident(a1,b2c2)
| incident(a2,b1c1) ),
inference(resolve,[status(thm)],[c_1274,c_54]) ).
cnf(c_10855,plain,
( point_equal(ab,a1)
| ~ incident(ab,a1b1)
| incident(c1,ob)
| incident(a1,b2c2)
| incident(a2,b1c1) ),
inference(resolve,[status(thm)],[c_1304,c_1217]) ).
cnf(c_1306,plain,
( point_equal(ab,a1)
| incident(c1,ob)
| incident(a1,b2c2)
| incident(a2,b1c1) ),
inference(resolve,[status(thm)],[c_53,c_10855]) ).
cnf(c_10856,plain,
( line_equal(a1c1,a1b1)
| point_equal(a1,ab)
| ~ incident(a1,a1c1)
| incident(c1,ob)
| incident(a1,b2c2)
| incident(a2,b1c1) ),
inference(resolve,[status(thm)],[c_1304,c_1149]) ).
cnf(c_10857,plain,
( line_equal(a1c1,a1b1)
| point_equal(a1,ab)
| incident(c1,ob)
| incident(a1,b2c2)
| incident(a2,b1c1) ),
inference(resolve,[status(thm)],[c_32,c_10856]) ).
cnf(c_1307,plain,
( point_equal(a1,ab)
| incident(c1,ob)
| incident(a1,b2c2)
| incident(a2,b1c1) ),
inference(resolve,[status(thm)],[c_274,c_10857]) ).
cnf(c_1392,plain,
( incident(ab,A)
| ~ incident(a1,A)
| incident(c1,ob)
| incident(a1,b2c2)
| incident(a2,b1c1) ),
inference(resolve,[status(thm)],[c_1306,c_69]) ).
cnf(c_1397,plain,
( point_equal(a1,A)
| ~ point_equal(ab,A)
| incident(c1,ob)
| incident(a1,b2c2)
| incident(a2,b1c1) ),
inference(resolve,[status(thm)],[c_1307,c_65]) ).
cnf(c_2052,plain,
( incident(ab,oa)
| incident(c1,ob)
| incident(a1,b2c2)
| incident(a2,b1c1) ),
inference(resolve,[status(thm)],[c_1392,c_43]) ).
cnf(c_10858,plain,
( line_equal(a2b2,oa)
| point_equal(ab,a2)
| ~ incident(ab,a2b2)
| incident(c1,ob)
| incident(a1,b2c2)
| incident(a2,b1c1) ),
inference(resolve,[status(thm)],[c_2052,c_1221]) ).
cnf(c_2054,plain,
( line_equal(a2b2,oa)
| point_equal(ab,a2)
| incident(c1,ob)
| incident(a1,b2c2)
| incident(a2,b1c1) ),
inference(resolve,[status(thm)],[c_54,c_10858]) ).
cnf(c_10859,plain,
( point_equal(a1,a2)
| incident(c1,ob)
| incident(a1,b2c2)
| incident(a2,b1c1)
| line_equal(a2b2,oa)
| incident(c1,ob)
| incident(a1,b2c2)
| incident(a2,b1c1) ),
inference(resolve,[status(thm)],[c_2054,c_1397]) ).
cnf(c_10860,plain,
( point_equal(a1,a2)
| incident(c1,ob)
| incident(a1,b2c2)
| line_equal(a2b2,oa)
| incident(c1,ob)
| incident(a1,b2c2)
| incident(a2,b1c1) ),
inference(copy,[status(thm)],[c_10859]) ).
cnf(c_10861,plain,
( point_equal(a1,a2)
| incident(c1,ob)
| line_equal(a2b2,oa)
| incident(c1,ob)
| incident(a1,b2c2)
| incident(a2,b1c1) ),
inference(copy,[status(thm)],[c_10860]) ).
cnf(c_10862,plain,
( point_equal(a1,a2)
| line_equal(a2b2,oa)
| incident(c1,ob)
| incident(a1,b2c2)
| incident(a2,b1c1) ),
inference(copy,[status(thm)],[c_10861]) ).
cnf(c_3089,plain,
( line_equal(a2b2,oa)
| incident(c1,ob)
| incident(a1,b2c2)
| incident(a2,b1c1) ),
inference(resolve,[status(thm)],[c_228,c_10862]) ).
cnf(c_3097,plain,
( line_equal(oa,a2b2)
| incident(c1,ob)
| incident(a1,b2c2)
| incident(a2,b1c1) ),
inference(resolve,[status(thm)],[c_3089,c_67]) ).
cnf(c_3102,plain,
( incident(A,a2b2)
| ~ incident(A,oa)
| incident(c1,ob)
| incident(a1,b2c2)
| incident(a2,b1c1) ),
inference(resolve,[status(thm)],[c_3097,c_70]) ).
cnf(c_3388,plain,
( incident(o,a2b2)
| incident(c1,ob)
| incident(a1,b2c2)
| incident(a2,b1c1) ),
inference(resolve,[status(thm)],[c_3102,c_40]) ).
cnf(c_10863,plain,
( incident(a2,b1c1)
| point_equal(c1,o)
| incident(c1,ob)
| incident(a1,b2c2)
| incident(a2,b1c1) ),
inference(resolve,[status(thm)],[c_3388,c_889]) ).
cnf(c_3401,plain,
( point_equal(c1,o)
| incident(c1,ob)
| incident(a1,b2c2)
| incident(a2,b1c1) ),
inference(copy,[status(thm)],[c_10863]) ).
cnf(c_3505,plain,
( incident(c1,A)
| ~ incident(o,A)
| incident(c1,ob)
| incident(a1,b2c2)
| incident(a2,b1c1) ),
inference(resolve,[status(thm)],[c_3401,c_69]) ).
cnf(c_10864,plain,
( ~ incident(o,ob)
| incident(c1,ob)
| incident(a1,b2c2)
| incident(a2,b1c1) ),
inference(factor,[status(thm)],[c_3505]) ).
cnf(c_3508,plain,
( incident(c1,ob)
| incident(a1,b2c2)
| incident(a2,b1c1) ),
inference(resolve,[status(thm)],[c_41,c_10864]) ).
cnf(c_10865,plain,
( line_equal(ob,b1c1)
| point_equal(c1,b1)
| ~ incident(c1,b1c1)
| incident(a1,b2c2)
| incident(a2,b1c1) ),
inference(resolve,[status(thm)],[c_3508,c_1183]) ).
cnf(c_10866,plain,
( line_equal(ob,b1c1)
| point_equal(c1,b1)
| incident(a1,b2c2)
| incident(a2,b1c1) ),
inference(resolve,[status(thm)],[c_36,c_10865]) ).
cnf(c_3514,plain,
( line_equal(ob,b1c1)
| incident(a1,b2c2)
| incident(a2,b1c1) ),
inference(resolve,[status(thm)],[c_276,c_10866]) ).
cnf(c_10867,plain,
( incident(a1,b2c2)
| point_equal(c1,b2)
| ~ incident(c1,a1c1)
| incident(a1,b2c2)
| incident(a2,b1c1) ),
inference(resolve,[status(thm)],[c_3508,c_1182]) ).
cnf(c_10868,plain,
( point_equal(c1,b2)
| ~ incident(c1,a1c1)
| incident(a1,b2c2)
| incident(a2,b1c1) ),
inference(copy,[status(thm)],[c_10867]) ).
cnf(c_3515,plain,
( point_equal(c1,b2)
| incident(a1,b2c2)
| incident(a2,b1c1) ),
inference(resolve,[status(thm)],[c_33,c_10868]) ).
cnf(c_3560,plain,
( incident(A,b1c1)
| ~ incident(A,ob)
| incident(a1,b2c2)
| incident(a2,b1c1) ),
inference(resolve,[status(thm)],[c_3514,c_70]) ).
cnf(c_3564,plain,
( incident(c1,A)
| ~ incident(b2,A)
| incident(a1,b2c2)
| incident(a2,b1c1) ),
inference(resolve,[status(thm)],[c_3515,c_69]) ).
cnf(c_3650,plain,
( incident(b2,b1c1)
| incident(a1,b2c2)
| incident(a2,b1c1) ),
inference(resolve,[status(thm)],[c_3560,c_46]) ).
cnf(c_3651,plain,
( incident(o,b1c1)
| incident(a1,b2c2)
| incident(a2,b1c1) ),
inference(resolve,[status(thm)],[c_3560,c_41]) ).
cnf(c_3655,plain,
( point_equal(bc,b2)
| incident(a1,b2c2)
| incident(a2,b1c1) ),
inference(resolve,[status(thm)],[c_3650,c_431]) ).
cnf(c_10869,plain,
( line_equal(b1c1,b2c2)
| point_equal(bc,o)
| ~ incident(o,b2c2)
| ~ incident(bc,b1c1)
| incident(a1,b2c2)
| incident(a2,b1c1) ),
inference(resolve,[status(thm)],[c_3651,c_137]) ).
cnf(c_10870,plain,
( line_equal(b1c1,b2c2)
| point_equal(bc,o)
| ~ incident(o,b2c2)
| incident(a1,b2c2)
| incident(a2,b1c1) ),
inference(resolve,[status(thm)],[c_49,c_10869]) ).
cnf(c_3726,plain,
( point_equal(bc,o)
| ~ incident(o,b2c2)
| incident(a1,b2c2)
| incident(a2,b1c1) ),
inference(resolve,[status(thm)],[c_75,c_10870]) ).
cnf(c_3749,plain,
( incident(bc,A)
| ~ incident(b2,A)
| incident(a1,b2c2)
| incident(a2,b1c1) ),
inference(resolve,[status(thm)],[c_3655,c_69]) ).
cnf(c_3752,plain,
( incident(c1,b2c2)
| incident(a1,b2c2)
| incident(a2,b1c1) ),
inference(resolve,[status(thm)],[c_3564,c_39]) ).
cnf(c_3756,plain,
( line_equal(oc,b2c2)
| incident(a1,b2c2)
| incident(a2,b1c1) ),
inference(resolve,[status(thm)],[c_3752,c_485]) ).
cnf(c_3787,plain,
( incident(A,b2c2)
| ~ incident(A,oc)
| incident(a1,b2c2)
| incident(a2,b1c1) ),
inference(resolve,[status(thm)],[c_3756,c_70]) ).
cnf(c_3845,plain,
( incident(bc,a2b2)
| incident(a1,b2c2)
| incident(a2,b1c1) ),
inference(resolve,[status(thm)],[c_3749,c_31]) ).
cnf(c_10871,plain,
( incident(a1,b2c2)
| incident(bc,a1c1)
| incident(a1,b2c2)
| incident(a2,b1c1) ),
inference(resolve,[status(thm)],[c_3749,c_25]) ).
cnf(c_3846,plain,
( incident(bc,a1c1)
| incident(a1,b2c2)
| incident(a2,b1c1) ),
inference(copy,[status(thm)],[c_10871]) ).
cnf(c_3890,plain,
( ~ incident(ac,a2b2)
| incident(a1,b2c2)
| incident(a2,b1c1) ),
inference(resolve,[status(thm)],[c_3845,c_253]) ).
cnf(c_10872,plain,
( line_equal(oa,a2b2)
| point_equal(bc,a2)
| ~ incident(a2,a2b2)
| ~ incident(bc,oa)
| incident(a1,b2c2)
| incident(a2,b1c1) ),
inference(resolve,[status(thm)],[c_3845,c_173]) ).
cnf(c_10873,plain,
( line_equal(oa,a2b2)
| point_equal(bc,a2)
| ~ incident(bc,oa)
| incident(a1,b2c2)
| incident(a2,b1c1) ),
inference(resolve,[status(thm)],[c_30,c_10872]) ).
cnf(c_3902,plain,
( line_equal(oa,a2b2)
| ~ incident(bc,oa)
| incident(a1,b2c2)
| incident(a2,b1c1) ),
inference(resolve,[status(thm)],[c_284,c_10873]) ).
cnf(c_10874,plain,
( line_equal(a1c1,oa)
| point_equal(bc,a1)
| ~ incident(a1,a1c1)
| ~ incident(bc,oa)
| incident(a1,b2c2)
| incident(a2,b1c1) ),
inference(resolve,[status(thm)],[c_3846,c_204]) ).
cnf(c_10875,plain,
( line_equal(a1c1,oa)
| point_equal(bc,a1)
| ~ incident(bc,oa)
| incident(a1,b2c2)
| incident(a2,b1c1) ),
inference(resolve,[status(thm)],[c_32,c_10874]) ).
cnf(c_3928,plain,
( line_equal(a1c1,oa)
| ~ incident(bc,oa)
| incident(a1,b2c2)
| incident(a2,b1c1) ),
inference(resolve,[status(thm)],[c_413,c_10875]) ).
cnf(c_3953,plain,
( incident(o,b2c2)
| incident(a1,b2c2)
| incident(a2,b1c1) ),
inference(resolve,[status(thm)],[c_3787,c_42]) ).
cnf(c_10876,plain,
( point_equal(bc,o)
| incident(a1,b2c2)
| incident(a2,b1c1)
| incident(a1,b2c2)
| incident(a2,b1c1) ),
inference(resolve,[status(thm)],[c_3953,c_3726]) ).
cnf(c_10877,plain,
( point_equal(bc,o)
| incident(a1,b2c2)
| incident(a1,b2c2)
| incident(a2,b1c1) ),
inference(copy,[status(thm)],[c_10876]) ).
cnf(c_3954,plain,
( point_equal(bc,o)
| incident(a1,b2c2)
| incident(a2,b1c1) ),
inference(copy,[status(thm)],[c_10877]) ).
cnf(c_4002,plain,
( incident(bc,A)
| ~ incident(o,A)
| incident(a1,b2c2)
| incident(a2,b1c1) ),
inference(resolve,[status(thm)],[c_3954,c_69]) ).
cnf(c_4022,plain,
( incident(bc,oa)
| incident(a1,b2c2)
| incident(a2,b1c1) ),
inference(resolve,[status(thm)],[c_4002,c_40]) ).
cnf(c_10878,plain,
( line_equal(a1c1,oa)
| incident(a1,b2c2)
| incident(a2,b1c1)
| incident(a1,b2c2)
| incident(a2,b1c1) ),
inference(resolve,[status(thm)],[c_4022,c_3928]) ).
cnf(c_10879,plain,
( line_equal(a1c1,oa)
| incident(a1,b2c2)
| incident(a1,b2c2)
| incident(a2,b1c1) ),
inference(copy,[status(thm)],[c_10878]) ).
cnf(c_4024,plain,
( line_equal(a1c1,oa)
| incident(a1,b2c2)
| incident(a2,b1c1) ),
inference(copy,[status(thm)],[c_10879]) ).
cnf(c_10880,plain,
( line_equal(oa,a2b2)
| incident(a1,b2c2)
| incident(a2,b1c1)
| incident(a1,b2c2)
| incident(a2,b1c1) ),
inference(resolve,[status(thm)],[c_4022,c_3902]) ).
cnf(c_10881,plain,
( line_equal(oa,a2b2)
| incident(a1,b2c2)
| incident(a1,b2c2)
| incident(a2,b1c1) ),
inference(copy,[status(thm)],[c_10880]) ).
cnf(c_4025,plain,
( line_equal(oa,a2b2)
| incident(a1,b2c2)
| incident(a2,b1c1) ),
inference(copy,[status(thm)],[c_10881]) ).
cnf(c_4049,plain,
( incident(A,oa)
| ~ incident(A,a1c1)
| incident(a1,b2c2)
| incident(a2,b1c1) ),
inference(resolve,[status(thm)],[c_4024,c_70]) ).
cnf(c_4052,plain,
( incident(A,a2b2)
| ~ incident(A,oa)
| incident(a1,b2c2)
| incident(a2,b1c1) ),
inference(resolve,[status(thm)],[c_4025,c_70]) ).
cnf(c_4279,plain,
( incident(ac,oa)
| incident(a1,b2c2)
| incident(a2,b1c1) ),
inference(resolve,[status(thm)],[c_4049,c_51]) ).
cnf(c_10882,plain,
( incident(a1,b2c2)
| incident(a2,b1c1)
| incident(ac,a2b2)
| incident(a1,b2c2)
| incident(a2,b1c1) ),
inference(resolve,[status(thm)],[c_4052,c_4279]) ).
cnf(c_10883,plain,
( incident(a1,b2c2)
| incident(ac,a2b2)
| incident(a1,b2c2)
| incident(a2,b1c1) ),
inference(copy,[status(thm)],[c_10882]) ).
cnf(c_4318,plain,
( incident(ac,a2b2)
| incident(a1,b2c2)
| incident(a2,b1c1) ),
inference(copy,[status(thm)],[c_10883]) ).
cnf(c_10884,plain,
( incident(a1,b2c2)
| incident(a2,b1c1)
| incident(a1,b2c2)
| incident(a2,b1c1) ),
inference(resolve,[status(thm)],[c_4318,c_3890]) ).
cnf(c_10885,plain,
( incident(a1,b2c2)
| incident(a1,b2c2)
| incident(a2,b1c1) ),
inference(copy,[status(thm)],[c_10884]) ).
cnf(c_4320,plain,
( incident(a1,b2c2)
| incident(a2,b1c1) ),
inference(copy,[status(thm)],[c_10885]) ).
cnf(c_10886,plain,
( incident(a1,b2c2)
| incident(b1,a2c2)
| incident(a1,b2c2) ),
inference(resolve,[status(thm)],[c_4320,c_607]) ).
cnf(c_4325,plain,
( incident(b1,a2c2)
| incident(a1,b2c2) ),
inference(copy,[status(thm)],[c_10886]) ).
cnf(c_10887,plain,
( line_equal(b1c1,oa)
| point_equal(a2,o)
| ~ incident(o,b1c1)
| ~ incident(a2,oa)
| incident(a1,b2c2) ),
inference(resolve,[status(thm)],[c_4320,c_207]) ).
cnf(c_10888,plain,
( line_equal(b1c1,oa)
| point_equal(a2,o)
| ~ incident(o,b1c1)
| incident(a1,b2c2) ),
inference(resolve,[status(thm)],[c_44,c_10887]) ).
cnf(c_4333,plain,
( point_equal(a2,o)
| ~ incident(o,b1c1)
| incident(a1,b2c2) ),
inference(resolve,[status(thm)],[c_389,c_10888]) ).
cnf(c_4375,plain,
( line_equal(b1c1,a2c2)
| point_equal(a2,b1)
| ~ incident(a2,b1c1)
| incident(a1,b2c2) ),
inference(resolve,[status(thm)],[c_4325,c_1108]) ).
cnf(c_10889,plain,
( line_equal(a2c2,ob)
| point_equal(b1,A)
| ~ incident(A,ob)
| ~ incident(A,a2c2)
| incident(a1,b2c2) ),
inference(resolve,[status(thm)],[c_4325,c_142]) ).
cnf(c_4415,plain,
( point_equal(b1,A)
| ~ incident(A,ob)
| ~ incident(A,a2c2)
| incident(a1,b2c2) ),
inference(resolve,[status(thm)],[c_313,c_10889]) ).
cnf(c_10890,plain,
( incident(a1,b2c2)
| line_equal(b1c1,a2c2)
| point_equal(a2,b1)
| incident(a1,b2c2) ),
inference(resolve,[status(thm)],[c_4375,c_4320]) ).
cnf(c_4431,plain,
( line_equal(b1c1,a2c2)
| point_equal(a2,b1)
| incident(a1,b2c2) ),
inference(copy,[status(thm)],[c_10890]) ).
cnf(c_4432,plain,
( incident(a2,A)
| ~ incident(b1,A)
| line_equal(b1c1,a2c2)
| incident(a1,b2c2) ),
inference(resolve,[status(thm)],[c_4431,c_69]) ).
cnf(c_4447,plain,
( incident(a2,ob)
| line_equal(b1c1,a2c2)
| incident(a1,b2c2) ),
inference(resolve,[status(thm)],[c_4432,c_45]) ).
cnf(c_4449,plain,
( incident(A,a2c2)
| ~ incident(A,b1c1)
| incident(a2,ob)
| incident(a1,b2c2) ),
inference(resolve,[status(thm)],[c_4447,c_70]) ).
cnf(c_4452,plain,
( line_equal(a2c2,b1c1)
| incident(a2,ob)
| incident(a1,b2c2) ),
inference(resolve,[status(thm)],[c_4447,c_67]) ).
cnf(c_4457,plain,
( incident(A,b1c1)
| ~ incident(A,a2c2)
| incident(a2,ob)
| incident(a1,b2c2) ),
inference(resolve,[status(thm)],[c_4452,c_70]) ).
cnf(c_4480,plain,
( incident(c1,a2c2)
| incident(a2,ob)
| incident(a1,b2c2) ),
inference(resolve,[status(thm)],[c_4449,c_36]) ).
cnf(c_4519,plain,
( line_equal(oc,a2c2)
| incident(a2,ob)
| incident(a1,b2c2) ),
inference(resolve,[status(thm)],[c_4480,c_487]) ).
cnf(c_4557,plain,
( incident(A,a2c2)
| ~ incident(A,oc)
| incident(a2,ob)
| incident(a1,b2c2) ),
inference(resolve,[status(thm)],[c_4519,c_70]) ).
cnf(c_5199,plain,
( incident(o,a2c2)
| incident(a2,ob)
| incident(a1,b2c2) ),
inference(resolve,[status(thm)],[c_4557,c_42]) ).
cnf(c_10891,plain,
( incident(o,b1c1)
| incident(a2,ob)
| incident(a1,b2c2)
| incident(a2,ob)
| incident(a1,b2c2) ),
inference(resolve,[status(thm)],[c_5199,c_4457]) ).
cnf(c_10892,plain,
( incident(o,b1c1)
| incident(a2,ob)
| incident(a2,ob)
| incident(a1,b2c2) ),
inference(copy,[status(thm)],[c_10891]) ).
cnf(c_5203,plain,
( incident(o,b1c1)
| incident(a2,ob)
| incident(a1,b2c2) ),
inference(copy,[status(thm)],[c_10892]) ).
cnf(c_10893,plain,
( point_equal(a2,o)
| incident(a1,b2c2)
| incident(a2,ob)
| incident(a1,b2c2) ),
inference(resolve,[status(thm)],[c_5203,c_4333]) ).
cnf(c_5251,plain,
( point_equal(a2,o)
| incident(a2,ob)
| incident(a1,b2c2) ),
inference(copy,[status(thm)],[c_10893]) ).
cnf(c_5291,plain,
( incident(a2,A)
| ~ incident(o,A)
| incident(a2,ob)
| incident(a1,b2c2) ),
inference(resolve,[status(thm)],[c_5251,c_69]) ).
cnf(c_10894,plain,
( ~ incident(o,ob)
| incident(a2,ob)
| incident(a1,b2c2) ),
inference(factor,[status(thm)],[c_5291]) ).
cnf(c_5294,plain,
( incident(a2,ob)
| incident(a1,b2c2) ),
inference(resolve,[status(thm)],[c_41,c_10894]) ).
cnf(c_10895,plain,
( point_equal(b1,a2)
| ~ incident(a2,a2c2)
| incident(a1,b2c2)
| incident(a1,b2c2) ),
inference(resolve,[status(thm)],[c_5294,c_4415]) ).
cnf(c_10896,plain,
( point_equal(b1,a2)
| ~ incident(a2,a2c2)
| incident(a1,b2c2) ),
inference(copy,[status(thm)],[c_10895]) ).
cnf(c_5295,plain,
( point_equal(b1,a2)
| incident(a1,b2c2) ),
inference(resolve,[status(thm)],[c_34,c_10896]) ).
cnf(c_10897,plain,
( line_equal(ob,a2b2)
| point_equal(a2,b2)
| ~ incident(a2,a2b2)
| incident(a1,b2c2) ),
inference(resolve,[status(thm)],[c_5294,c_1181]) ).
cnf(c_10898,plain,
( line_equal(ob,a2b2)
| point_equal(a2,b2)
| incident(a1,b2c2) ),
inference(resolve,[status(thm)],[c_30,c_10897]) ).
cnf(c_5301,plain,
( line_equal(ob,a2b2)
| incident(a1,b2c2) ),
inference(resolve,[status(thm)],[c_245,c_10898]) ).
cnf(c_5335,plain,
( incident(b1,A)
| ~ incident(a2,A)
| incident(a1,b2c2) ),
inference(resolve,[status(thm)],[c_5295,c_69]) ).
cnf(c_5344,plain,
( incident(A,a2b2)
| ~ incident(A,ob)
| incident(a1,b2c2) ),
inference(resolve,[status(thm)],[c_5301,c_70]) ).
cnf(c_5367,plain,
( incident(b1,oa)
| incident(a1,b2c2) ),
inference(resolve,[status(thm)],[c_5335,c_44]) ).
cnf(c_5368,plain,
( incident(b1,a2b2)
| incident(a1,b2c2) ),
inference(resolve,[status(thm)],[c_5335,c_30]) ).
cnf(c_10899,plain,
( line_equal(oa,a1b1)
| point_equal(b1,a1)
| ~ incident(b1,a1b1)
| incident(a1,b2c2) ),
inference(resolve,[status(thm)],[c_5367,c_1188]) ).
cnf(c_10900,plain,
( line_equal(oa,a1b1)
| point_equal(b1,a1)
| incident(a1,b2c2) ),
inference(resolve,[status(thm)],[c_29,c_10899]) ).
cnf(c_5370,plain,
( line_equal(oa,a1b1)
| incident(a1,b2c2) ),
inference(resolve,[status(thm)],[c_271,c_10900]) ).
cnf(c_5409,plain,
( point_equal(ab,b1)
| incident(a1,b2c2) ),
inference(resolve,[status(thm)],[c_5368,c_310]) ).
cnf(c_5440,plain,
( incident(A,a1b1)
| ~ incident(A,oa)
| incident(a1,b2c2) ),
inference(resolve,[status(thm)],[c_5370,c_70]) ).
cnf(c_5450,plain,
( incident(ab,A)
| ~ incident(b1,A)
| incident(a1,b2c2) ),
inference(resolve,[status(thm)],[c_5409,c_69]) ).
cnf(c_5531,plain,
( incident(o,a2b2)
| incident(a1,b2c2) ),
inference(resolve,[status(thm)],[c_5344,c_41]) ).
cnf(c_5532,plain,
( point_equal(o,ab)
| ~ incident(o,a1b1)
| incident(a1,b2c2) ),
inference(resolve,[status(thm)],[c_5531,c_1171]) ).
cnf(c_5642,plain,
( incident(o,a1b1)
| incident(a1,b2c2) ),
inference(resolve,[status(thm)],[c_5440,c_40]) ).
cnf(c_10901,plain,
( incident(a1,b2c2)
| incident(ab,a2c2)
| incident(a1,b2c2) ),
inference(resolve,[status(thm)],[c_5450,c_4325]) ).
cnf(c_5701,plain,
( incident(ab,a2c2)
| incident(a1,b2c2) ),
inference(copy,[status(thm)],[c_10901]) ).
cnf(c_5702,plain,
( incident(ab,b1c1)
| incident(a1,b2c2) ),
inference(resolve,[status(thm)],[c_5450,c_37]) ).
cnf(c_10902,plain,
( line_equal(oc,a2c2)
| point_equal(ab,c2)
| ~ incident(c2,a2c2)
| ~ incident(ab,oc)
| incident(a1,b2c2) ),
inference(resolve,[status(thm)],[c_5701,c_169]) ).
cnf(c_10903,plain,
( line_equal(oc,a2c2)
| point_equal(ab,c2)
| ~ incident(ab,oc)
| incident(a1,b2c2) ),
inference(resolve,[status(thm)],[c_35,c_10902]) ).
cnf(c_5717,plain,
( line_equal(oc,a2c2)
| ~ incident(ab,oc)
| incident(a1,b2c2) ),
inference(resolve,[status(thm)],[c_362,c_10903]) ).
cnf(c_10904,plain,
( line_equal(b1c1,oc)
| point_equal(ab,c1)
| ~ incident(c1,b1c1)
| ~ incident(ab,oc)
| incident(a1,b2c2) ),
inference(resolve,[status(thm)],[c_5702,c_200]) ).
cnf(c_10905,plain,
( line_equal(b1c1,oc)
| point_equal(ab,c1)
| ~ incident(ab,oc)
| incident(a1,b2c2) ),
inference(resolve,[status(thm)],[c_36,c_10904]) ).
cnf(c_5739,plain,
( line_equal(b1c1,oc)
| ~ incident(ab,oc)
| incident(a1,b2c2) ),
inference(resolve,[status(thm)],[c_492,c_10905]) ).
cnf(c_10906,plain,
( incident(a1,b2c2)
| point_equal(o,ab)
| incident(a1,b2c2) ),
inference(resolve,[status(thm)],[c_5532,c_5642]) ).
cnf(c_5766,plain,
( point_equal(o,ab)
| incident(a1,b2c2) ),
inference(copy,[status(thm)],[c_10906]) ).
cnf(c_5772,plain,
( point_equal(ab,o)
| incident(a1,b2c2) ),
inference(resolve,[status(thm)],[c_5766,c_64]) ).
cnf(c_5781,plain,
( incident(ab,A)
| ~ incident(o,A)
| incident(a1,b2c2) ),
inference(resolve,[status(thm)],[c_5772,c_69]) ).
cnf(c_5884,plain,
( incident(ab,oc)
| incident(a1,b2c2) ),
inference(resolve,[status(thm)],[c_5781,c_42]) ).
cnf(c_10907,plain,
( line_equal(b1c1,oc)
| incident(a1,b2c2)
| incident(a1,b2c2) ),
inference(resolve,[status(thm)],[c_5884,c_5739]) ).
cnf(c_5886,plain,
( line_equal(b1c1,oc)
| incident(a1,b2c2) ),
inference(copy,[status(thm)],[c_10907]) ).
cnf(c_10908,plain,
( line_equal(oc,a2c2)
| incident(a1,b2c2)
| incident(a1,b2c2) ),
inference(resolve,[status(thm)],[c_5884,c_5717]) ).
cnf(c_5887,plain,
( line_equal(oc,a2c2)
| incident(a1,b2c2) ),
inference(copy,[status(thm)],[c_10908]) ).
cnf(c_5912,plain,
( incident(A,oc)
| ~ incident(A,b1c1)
| incident(a1,b2c2) ),
inference(resolve,[status(thm)],[c_5886,c_70]) ).
cnf(c_5915,plain,
( incident(A,a2c2)
| ~ incident(A,oc)
| incident(a1,b2c2) ),
inference(resolve,[status(thm)],[c_5887,c_70]) ).
cnf(c_5993,plain,
( incident(bc,oc)
| incident(a1,b2c2) ),
inference(resolve,[status(thm)],[c_5912,c_49]) ).
cnf(c_10909,plain,
( incident(a1,b2c2)
| incident(bc,a2c2)
| incident(a1,b2c2) ),
inference(resolve,[status(thm)],[c_5915,c_5993]) ).
cnf(c_6030,plain,
( incident(bc,a2c2)
| incident(a1,b2c2) ),
inference(copy,[status(thm)],[c_10909]) ).
cnf(c_6037,plain,
( ~ incident(ab,a2c2)
| incident(a1,b2c2) ),
inference(resolve,[status(thm)],[c_6030,c_279]) ).
cnf(c_10910,plain,
( incident(a1,b2c2)
| incident(a1,b2c2) ),
inference(resolve,[status(thm)],[c_6037,c_5701]) ).
cnf(c_6075,plain,
incident(a1,b2c2),
inference(copy,[status(thm)],[c_10910]) ).
cnf(c_6077,plain,
( incident(b1,a2c2)
| line_equal(a1b1,b2c2)
| point_equal(c2,a1) ),
inference(resolve,[status(thm)],[c_6075,c_1256]) ).
cnf(c_6105,plain,
( incident(a2,b1c1)
| ~ incident(b1,a2c2) ),
inference(resolve,[status(thm)],[c_6075,c_240]) ).
cnf(c_6106,negated_conjecture,
( ~ incident(c1,a2b2)
| ~ incident(b1,a2c2) ),
inference(resolve,[status(thm)],[c_6075,c_82]) ).
cnf(c_6148,plain,
( line_equal(b2c2,A)
| point_equal(c2,a1)
| ~ incident(a1,A)
| ~ incident(c2,A) ),
inference(resolve,[status(thm)],[c_6075,c_119]) ).
cnf(c_6171,plain,
( incident(c2,A)
| ~ incident(a1,A)
| incident(b1,a2c2)
| line_equal(a1b1,b2c2) ),
inference(resolve,[status(thm)],[c_6077,c_69]) ).
cnf(c_6196,plain,
( incident(c2,oa)
| incident(b1,a2c2)
| line_equal(a1b1,b2c2) ),
inference(resolve,[status(thm)],[c_6171,c_43]) ).
cnf(c_6198,plain,
( incident(A,b2c2)
| ~ incident(A,a1b1)
| incident(c2,oa)
| incident(b1,a2c2) ),
inference(resolve,[status(thm)],[c_6196,c_70]) ).
cnf(c_6486,plain,
( incident(ab,b2c2)
| incident(c2,oa)
| incident(b1,a2c2) ),
inference(resolve,[status(thm)],[c_6198,c_53]) ).
cnf(c_10911,plain,
( point_equal(ab,b2)
| ~ incident(ab,a2b2)
| incident(c2,oa)
| incident(b1,a2c2) ),
inference(resolve,[status(thm)],[c_6486,c_1196]) ).
cnf(c_6489,plain,
( point_equal(ab,b2)
| incident(c2,oa)
| incident(b1,a2c2) ),
inference(resolve,[status(thm)],[c_54,c_10911]) ).
cnf(c_10912,plain,
( line_equal(b2c2,a2b2)
| point_equal(b2,ab)
| ~ incident(b2,b2c2)
| incident(c2,oa)
| incident(b1,a2c2) ),
inference(resolve,[status(thm)],[c_6486,c_1129]) ).
cnf(c_10913,plain,
( line_equal(b2c2,a2b2)
| point_equal(b2,ab)
| incident(c2,oa)
| incident(b1,a2c2) ),
inference(resolve,[status(thm)],[c_39,c_10912]) ).
cnf(c_6491,plain,
( point_equal(b2,ab)
| incident(c2,oa)
| incident(b1,a2c2) ),
inference(resolve,[status(thm)],[c_255,c_10913]) ).
cnf(c_6567,plain,
( incident(ab,A)
| ~ incident(b2,A)
| incident(c2,oa)
| incident(b1,a2c2) ),
inference(resolve,[status(thm)],[c_6489,c_69]) ).
cnf(c_6572,plain,
( point_equal(b2,A)
| ~ point_equal(ab,A)
| incident(c2,oa)
| incident(b1,a2c2) ),
inference(resolve,[status(thm)],[c_6491,c_65]) ).
cnf(c_7584,plain,
( incident(ab,ob)
| incident(c2,oa)
| incident(b1,a2c2) ),
inference(resolve,[status(thm)],[c_6567,c_46]) ).
cnf(c_10914,plain,
( line_equal(a1b1,ob)
| point_equal(ab,b1)
| ~ incident(ab,a1b1)
| incident(c2,oa)
| incident(b1,a2c2) ),
inference(resolve,[status(thm)],[c_7584,c_1222]) ).
cnf(c_7585,plain,
( line_equal(a1b1,ob)
| point_equal(ab,b1)
| incident(c2,oa)
| incident(b1,a2c2) ),
inference(resolve,[status(thm)],[c_53,c_10914]) ).
cnf(c_10915,plain,
( point_equal(b2,b1)
| incident(c2,oa)
| incident(b1,a2c2)
| line_equal(a1b1,ob)
| incident(c2,oa)
| incident(b1,a2c2) ),
inference(resolve,[status(thm)],[c_7585,c_6572]) ).
cnf(c_10916,plain,
( point_equal(b2,b1)
| incident(c2,oa)
| line_equal(a1b1,ob)
| incident(c2,oa)
| incident(b1,a2c2) ),
inference(copy,[status(thm)],[c_10915]) ).
cnf(c_10917,plain,
( point_equal(b2,b1)
| line_equal(a1b1,ob)
| incident(c2,oa)
| incident(b1,a2c2) ),
inference(copy,[status(thm)],[c_10916]) ).
cnf(c_8468,plain,
( line_equal(a1b1,ob)
| incident(c2,oa)
| incident(b1,a2c2) ),
inference(resolve,[status(thm)],[c_77,c_10917]) ).
cnf(c_8474,plain,
( line_equal(ob,a1b1)
| incident(c2,oa)
| incident(b1,a2c2) ),
inference(resolve,[status(thm)],[c_8468,c_67]) ).
cnf(c_8479,plain,
( incident(A,a1b1)
| ~ incident(A,ob)
| incident(c2,oa)
| incident(b1,a2c2) ),
inference(resolve,[status(thm)],[c_8474,c_70]) ).
cnf(c_8719,plain,
( incident(o,a1b1)
| incident(c2,oa)
| incident(b1,a2c2) ),
inference(resolve,[status(thm)],[c_8479,c_41]) ).
cnf(c_10918,plain,
( incident(b1,a2c2)
| point_equal(c2,o)
| incident(c2,oa)
| incident(b1,a2c2) ),
inference(resolve,[status(thm)],[c_8719,c_903]) ).
cnf(c_8731,plain,
( point_equal(c2,o)
| incident(c2,oa)
| incident(b1,a2c2) ),
inference(copy,[status(thm)],[c_10918]) ).
cnf(c_8804,plain,
( incident(c2,A)
| ~ incident(o,A)
| incident(c2,oa)
| incident(b1,a2c2) ),
inference(resolve,[status(thm)],[c_8731,c_69]) ).
cnf(c_10919,plain,
( ~ incident(o,oa)
| incident(c2,oa)
| incident(b1,a2c2) ),
inference(factor,[status(thm)],[c_8804]) ).
cnf(c_8807,plain,
( incident(c2,oa)
| incident(b1,a2c2) ),
inference(resolve,[status(thm)],[c_40,c_10919]) ).
cnf(c_10920,plain,
( line_equal(b2c2,oa)
| point_equal(c2,a1)
| ~ incident(a1,oa)
| incident(b1,a2c2) ),
inference(resolve,[status(thm)],[c_8807,c_6148]) ).
cnf(c_10921,plain,
( line_equal(b2c2,oa)
| point_equal(c2,a1)
| incident(b1,a2c2) ),
inference(resolve,[status(thm)],[c_43,c_10920]) ).
cnf(c_8808,plain,
( point_equal(c2,a1)
| incident(b1,a2c2) ),
inference(resolve,[status(thm)],[c_283,c_10921]) ).
cnf(c_10922,plain,
( line_equal(oa,a2c2)
| point_equal(c2,a2)
| ~ incident(c2,a2c2)
| incident(b1,a2c2) ),
inference(resolve,[status(thm)],[c_8807,c_1185]) ).
cnf(c_10923,plain,
( line_equal(oa,a2c2)
| point_equal(c2,a2)
| incident(b1,a2c2) ),
inference(resolve,[status(thm)],[c_35,c_10922]) ).
cnf(c_8811,plain,
( line_equal(oa,a2c2)
| incident(b1,a2c2) ),
inference(resolve,[status(thm)],[c_259,c_10923]) ).
cnf(c_8852,plain,
( incident(c2,A)
| ~ incident(a1,A)
| incident(b1,a2c2) ),
inference(resolve,[status(thm)],[c_8808,c_69]) ).
cnf(c_8861,plain,
( incident(A,a2c2)
| ~ incident(A,oa)
| incident(b1,a2c2) ),
inference(resolve,[status(thm)],[c_8811,c_70]) ).
cnf(c_8885,plain,
( incident(c2,a1c1)
| incident(b1,a2c2) ),
inference(resolve,[status(thm)],[c_8852,c_32]) ).
cnf(c_8892,plain,
( line_equal(oc,a1c1)
| incident(b1,a2c2) ),
inference(resolve,[status(thm)],[c_8885,c_465]) ).
cnf(c_8893,plain,
( point_equal(ac,c2)
| incident(b1,a2c2) ),
inference(resolve,[status(thm)],[c_8885,c_384]) ).
cnf(c_8925,plain,
( incident(A,a1c1)
| ~ incident(A,oc)
| incident(b1,a2c2) ),
inference(resolve,[status(thm)],[c_8892,c_70]) ).
cnf(c_8930,plain,
( incident(ac,A)
| ~ incident(c2,A)
| incident(b1,a2c2) ),
inference(resolve,[status(thm)],[c_8893,c_69]) ).
cnf(c_8982,plain,
( incident(o,a2c2)
| incident(b1,a2c2) ),
inference(resolve,[status(thm)],[c_8861,c_40]) ).
cnf(c_8984,plain,
( point_equal(o,ac)
| ~ incident(o,a1c1)
| incident(b1,a2c2) ),
inference(resolve,[status(thm)],[c_8982,c_1172]) ).
cnf(c_9083,plain,
( incident(o,a1c1)
| incident(b1,a2c2) ),
inference(resolve,[status(thm)],[c_8925,c_42]) ).
cnf(c_9135,plain,
( incident(ac,b2c2)
| incident(b1,a2c2) ),
inference(resolve,[status(thm)],[c_8930,c_38]) ).
cnf(c_10924,plain,
( incident(b1,a2c2)
| incident(ac,a1b1)
| incident(b1,a2c2) ),
inference(resolve,[status(thm)],[c_8930,c_26]) ).
cnf(c_9136,plain,
( incident(ac,a1b1)
| incident(b1,a2c2) ),
inference(copy,[status(thm)],[c_10924]) ).
cnf(c_9140,plain,
( ~ incident(ab,b2c2)
| incident(b1,a2c2) ),
inference(resolve,[status(thm)],[c_9135,c_281]) ).
cnf(c_10925,plain,
( line_equal(ob,b2c2)
| point_equal(ac,b2)
| ~ incident(b2,b2c2)
| ~ incident(ac,ob)
| incident(b1,a2c2) ),
inference(resolve,[status(thm)],[c_9135,c_171]) ).
cnf(c_10926,plain,
( line_equal(ob,b2c2)
| point_equal(ac,b2)
| ~ incident(ac,ob)
| incident(b1,a2c2) ),
inference(resolve,[status(thm)],[c_39,c_10925]) ).
cnf(c_9151,plain,
( line_equal(ob,b2c2)
| ~ incident(ac,ob)
| incident(b1,a2c2) ),
inference(resolve,[status(thm)],[c_335,c_10926]) ).
cnf(c_10927,plain,
( line_equal(a1b1,ob)
| point_equal(ac,b1)
| ~ incident(b1,a1b1)
| ~ incident(ac,ob)
| incident(b1,a2c2) ),
inference(resolve,[status(thm)],[c_9136,c_202]) ).
cnf(c_10928,plain,
( line_equal(a1b1,ob)
| point_equal(ac,b1)
| ~ incident(ac,ob)
| incident(b1,a2c2) ),
inference(resolve,[status(thm)],[c_29,c_10927]) ).
cnf(c_9176,plain,
( line_equal(a1b1,ob)
| ~ incident(ac,ob)
| incident(b1,a2c2) ),
inference(resolve,[status(thm)],[c_441,c_10928]) ).
cnf(c_10929,plain,
( incident(b1,a2c2)
| point_equal(o,ac)
| incident(b1,a2c2) ),
inference(resolve,[status(thm)],[c_8984,c_9083]) ).
cnf(c_9211,plain,
( point_equal(o,ac)
| incident(b1,a2c2) ),
inference(copy,[status(thm)],[c_10929]) ).
cnf(c_9217,plain,
( point_equal(ac,o)
| incident(b1,a2c2) ),
inference(resolve,[status(thm)],[c_9211,c_64]) ).
cnf(c_9226,plain,
( incident(ac,A)
| ~ incident(o,A)
| incident(b1,a2c2) ),
inference(resolve,[status(thm)],[c_9217,c_69]) ).
cnf(c_9313,plain,
( incident(ac,ob)
| incident(b1,a2c2) ),
inference(resolve,[status(thm)],[c_9226,c_41]) ).
cnf(c_10930,plain,
( line_equal(a1b1,ob)
| incident(b1,a2c2)
| incident(b1,a2c2) ),
inference(resolve,[status(thm)],[c_9313,c_9176]) ).
cnf(c_9315,plain,
( line_equal(a1b1,ob)
| incident(b1,a2c2) ),
inference(copy,[status(thm)],[c_10930]) ).
cnf(c_10931,plain,
( line_equal(ob,b2c2)
| incident(b1,a2c2)
| incident(b1,a2c2) ),
inference(resolve,[status(thm)],[c_9313,c_9151]) ).
cnf(c_9316,plain,
( line_equal(ob,b2c2)
| incident(b1,a2c2) ),
inference(copy,[status(thm)],[c_10931]) ).
cnf(c_9340,plain,
( incident(A,ob)
| ~ incident(A,a1b1)
| incident(b1,a2c2) ),
inference(resolve,[status(thm)],[c_9315,c_70]) ).
cnf(c_9343,plain,
( incident(A,b2c2)
| ~ incident(A,ob)
| incident(b1,a2c2) ),
inference(resolve,[status(thm)],[c_9316,c_70]) ).
cnf(c_9521,plain,
( incident(ab,ob)
| incident(b1,a2c2) ),
inference(resolve,[status(thm)],[c_9340,c_53]) ).
cnf(c_10932,plain,
( incident(b1,a2c2)
| incident(ab,b2c2)
| incident(b1,a2c2) ),
inference(resolve,[status(thm)],[c_9343,c_9521]) ).
cnf(c_9558,plain,
( incident(ab,b2c2)
| incident(b1,a2c2) ),
inference(copy,[status(thm)],[c_10932]) ).
cnf(c_10933,plain,
( incident(b1,a2c2)
| incident(b1,a2c2) ),
inference(resolve,[status(thm)],[c_9558,c_9140]) ).
cnf(c_9560,plain,
incident(b1,a2c2),
inference(copy,[status(thm)],[c_10933]) ).
cnf(c_9561,negated_conjecture,
~ incident(c1,a2b2),
inference(resolve,[status(thm)],[c_9560,c_6106]) ).
cnf(c_9562,plain,
incident(a2,b1c1),
inference(resolve,[status(thm)],[c_9560,c_6105]) ).
cnf(c_10934,plain,
( line_equal(b1c1,a2c2)
| point_equal(a2,b1)
| ~ incident(b1,a2c2) ),
inference(resolve,[status(thm)],[c_9562,c_1108]) ).
cnf(c_9566,plain,
( line_equal(b1c1,a2c2)
| point_equal(a2,b1) ),
inference(resolve,[status(thm)],[c_9560,c_10934]) ).
cnf(c_9583,plain,
( point_equal(b1,a2)
| ~ incident(a2,ob) ),
inference(resolve,[status(thm)],[c_9560,c_534]) ).
cnf(c_9597,plain,
( point_equal(c1,a2)
| ~ incident(c1,oa) ),
inference(resolve,[status(thm)],[c_9562,c_724]) ).
cnf(c_10935,plain,
( line_equal(b1c1,oc)
| point_equal(c1,a2)
| ~ incident(a2,oc)
| ~ incident(c1,b1c1) ),
inference(resolve,[status(thm)],[c_9562,c_140]) ).
cnf(c_9679,plain,
( line_equal(b1c1,oc)
| point_equal(c1,a2)
| ~ incident(a2,oc) ),
inference(resolve,[status(thm)],[c_36,c_10935]) ).
cnf(c_10936,plain,
( incident(A,a2b2)
| ~ point_equal(A,a2) ),
inference(resolve,[status(thm)],[c_69,c_30]) ).
cnf(c_9694,plain,
~ point_equal(c1,a2),
inference(resolve,[status(thm)],[c_10936,c_9561]) ).
cnf(c_9710,plain,
( line_equal(b1c1,oc)
| ~ incident(a2,oc) ),
inference(resolve,[status(thm)],[c_9694,c_9679]) ).
cnf(c_9713,plain,
~ incident(c1,oa),
inference(resolve,[status(thm)],[c_9694,c_9597]) ).
cnf(c_9725,plain,
( incident(a2,A)
| ~ incident(b1,A)
| line_equal(b1c1,a2c2) ),
inference(resolve,[status(thm)],[c_9566,c_69]) ).
cnf(c_10937,plain,
( incident(c1,A)
| ~ line_equal(oc,A) ),
inference(resolve,[status(thm)],[c_70,c_47]) ).
cnf(c_9770,plain,
~ line_equal(oc,oa),
inference(resolve,[status(thm)],[c_10937,c_9713]) ).
cnf(c_9776,plain,
( point_equal(a2,o)
| ~ incident(a2,oc) ),
inference(resolve,[status(thm)],[c_9770,c_1022]) ).
cnf(c_9808,plain,
( incident(a2,ob)
| line_equal(b1c1,a2c2) ),
inference(resolve,[status(thm)],[c_9725,c_45]) ).
cnf(c_9810,plain,
( incident(A,a2c2)
| ~ incident(A,b1c1)
| incident(a2,ob) ),
inference(resolve,[status(thm)],[c_9808,c_70]) ).
cnf(c_9841,plain,
( incident(c1,a2c2)
| incident(a2,ob) ),
inference(resolve,[status(thm)],[c_9810,c_36]) ).
cnf(c_9866,plain,
( line_equal(a2c2,oc)
| incident(a2,ob) ),
inference(resolve,[status(thm)],[c_9841,c_740]) ).
cnf(c_9889,plain,
( incident(A,oc)
| ~ incident(A,a2c2)
| incident(a2,ob) ),
inference(resolve,[status(thm)],[c_9866,c_70]) ).
cnf(c_10259,plain,
( incident(a2,oc)
| incident(a2,ob) ),
inference(resolve,[status(thm)],[c_9889,c_34]) ).
cnf(c_10296,plain,
( point_equal(a2,o)
| incident(a2,ob) ),
inference(resolve,[status(thm)],[c_10259,c_9776]) ).
cnf(c_10320,plain,
( incident(a2,A)
| ~ incident(o,A)
| incident(a2,ob) ),
inference(resolve,[status(thm)],[c_10296,c_69]) ).
cnf(c_10938,plain,
( ~ incident(o,ob)
| incident(a2,ob) ),
inference(factor,[status(thm)],[c_10320]) ).
cnf(c_10323,plain,
incident(a2,ob),
inference(resolve,[status(thm)],[c_41,c_10938]) ).
cnf(c_10324,plain,
point_equal(b1,a2),
inference(resolve,[status(thm)],[c_10323,c_9583]) ).
cnf(c_10328,plain,
line_equal(a2b2,ob),
inference(resolve,[status(thm)],[c_10323,c_835]) ).
cnf(c_10332,plain,
( line_equal(oa,ob)
| point_equal(a2,o) ),
inference(resolve,[status(thm)],[c_10323,c_551]) ).
cnf(c_10364,plain,
( incident(b1,A)
| ~ incident(a2,A) ),
inference(resolve,[status(thm)],[c_10324,c_69]) ).
cnf(c_10939,plain,
( line_equal(a2b2,A)
| ~ line_equal(ob,A) ),
inference(resolve,[status(thm)],[c_68,c_10328]) ).
cnf(c_10415,plain,
~ line_equal(ob,a1b1),
inference(resolve,[status(thm)],[c_10939,c_223]) ).
cnf(c_10422,plain,
~ incident(a1,ob),
inference(resolve,[status(thm)],[c_10415,c_536]) ).
cnf(c_10462,plain,
( incident(a2,A)
| ~ incident(o,A)
| line_equal(oa,ob) ),
inference(resolve,[status(thm)],[c_10332,c_69]) ).
cnf(c_10940,plain,
( incident(a1,A)
| ~ line_equal(oa,A) ),
inference(resolve,[status(thm)],[c_70,c_43]) ).
cnf(c_10466,plain,
~ line_equal(oa,ob),
inference(resolve,[status(thm)],[c_10940,c_10422]) ).
cnf(c_10471,plain,
( incident(a2,A)
| ~ incident(o,A) ),
inference(resolve,[status(thm)],[c_10466,c_10462]) ).
cnf(c_10511,plain,
incident(b1,a2b2),
inference(resolve,[status(thm)],[c_10364,c_30]) ).
cnf(c_10517,plain,
point_equal(ab,b1),
inference(resolve,[status(thm)],[c_10511,c_310]) ).
cnf(c_10584,plain,
( incident(ab,A)
| ~ incident(b1,A) ),
inference(resolve,[status(thm)],[c_10517,c_69]) ).
cnf(c_10674,plain,
incident(a2,oc),
inference(resolve,[status(thm)],[c_10471,c_42]) ).
cnf(c_10675,plain,
line_equal(b1c1,oc),
inference(resolve,[status(thm)],[c_10674,c_9710]) ).
cnf(c_10678,plain,
line_equal(oc,a2c2),
inference(resolve,[status(thm)],[c_10674,c_464]) ).
cnf(c_10771,plain,
incident(ab,a2c2),
inference(resolve,[status(thm)],[c_10584,c_9560]) ).
cnf(c_10774,plain,
~ incident(bc,a2c2),
inference(resolve,[status(thm)],[c_10771,c_279]) ).
cnf(c_10941,plain,
( incident(A,a2c2)
| ~ incident(A,oc) ),
inference(resolve,[status(thm)],[c_70,c_10678]) ).
cnf(c_10776,plain,
~ incident(bc,oc),
inference(resolve,[status(thm)],[c_10941,c_10774]) ).
cnf(c_10942,plain,
( incident(A,oc)
| ~ incident(A,b1c1) ),
inference(resolve,[status(thm)],[c_70,c_10675]) ).
cnf(c_10943,plain,
~ incident(bc,b1c1),
inference(resolve,[status(thm)],[c_10942,c_10776]) ).
cnf(c_10792,plain,
$false,
inference(resolve,[status(thm)],[c_49,c_10943]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO169+1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.07/0.35 % Computer : n004.cluster.edu
% 0.07/0.35 % Model : x86_64 x86_64
% 0.07/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.35 % Memory : 8046.5625MB
% 0.07/0.35 % OS : Linux 6.8.0-71-generic
% 0.07/0.35 % CPULimit : 300
% 0.07/0.35 % WCLimit : 300
% 0.07/0.35 % DateTime : Fri Sep 25 12:59:50 UTC 2026
% 0.07/0.36 % CPUTime :
% 0.12/0.36 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.12/0.36 % Process 3215503 was started by sandbox2 on n004,
% 0.12/0.36 % Fri Sep 25 12:59:50 2026
% 0.12/0.36 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.12/0.36
% 0.12/0.36 % From the command line: assign(max_seconds, 300).
% 74.55/10.19
% 74.55/10.19 % given #500 (A,wt=15): 172 -incident(A,ob) | -incident(A,B) | -incident(b1,B) | point_equal(A,b1) | line_equal(ob,B). [resolve(71,c,45,a)].
% 74.55/10.19
% 74.55/10.19 % given #1000 (A,wt=12): 1029 -incident(a1,oc) | -incident(c2,oa) | point_equal(a1,c2) | line_equal(oc,oa). [resolve(144,b,48,a)].
% 74.55/10.19
% 74.55/10.19 % given #1500 (A,wt=21): 1367 incident(a2,b1c1) | incident(a1,b2c2) | incident(a2,a1c1) | -incident(A,ob) | -incident(A,oc) | point_equal(A,c1) | line_equal(ob,oc). [resolve(1305,c,200,c)].
% 74.55/10.19
% 74.55/10.19 % given #2000 (A,wt=21): 1543 incident(a2,b1c1) | incident(a1,b2c2) | incident(c1,ob) | -incident(ab,A) | -incident(ac,A) | point_equal(ab,ac) | line_equal(a2b2,A). [resolve(1508,d,103,b)].
% 74.55/10.19
% 74.55/10.19 % given #2500 (A,wt=18): 1731 incident(a1,b2c2) | incident(a2,b1c1) | incident(b2,oc) | -incident(ac,A) | -incident(b2,A) | line_equal(a2b2,A). [resolve(1710,d,186,a),unit_del(f,335)].
% 74.55/10.19
% 74.55/10.19 % given #3000 (T,wt=12): 4963 incident(a1,b2c2) | incident(b1,oa) | -incident(ac,ob) | line_equal(ob,b1c1). [resolve(4949,c,172,b),unit_del(d,37),unit_del(e,441)].
% 74.55/10.19
% 74.55/10.19 % given #3500 (T,wt=12): 6221 incident(b1,a2c2) | incident(a1,oc) | -incident(bc,a2b2) | -incident(a2,a1b1). [resolve(6212,c,217,a),unit_del(e,284),unit_del(f,73)].
% 74.55/10.19
% 74.55/10.19 % given #4000 (T,wt=12): 7250 incident(a1,oc) | -incident(a2,oc) | point_equal(c1,a2) | line_equal(b1c1,oc). [resolve(7155,b,140,b),unit_del(b,36)].
% 74.55/10.19
% 74.55/10.19 % given #4500 (T,wt=6): 8885 incident(b1,a2c2) | incident(c2,a1c1). [resolve(8852,b,32,a)].
% 74.55/10.19
% 74.55/10.19 % given #5000 (A,wt=24): 2602 incident(a2,b1c1) | incident(a1,b2c2) | incident(a1,a2b2) | -incident(A,b1c1) | -incident(A,B) | -incident(o,B) | point_equal(A,o) | line_equal(b1c1,B). [resolve(2544,d,71,c)].
% 74.55/10.19
% 74.55/10.19 % SZS status Theorem for theBenchmark
% 74.55/10.19
% 74.55/10.19 % Proof 1 at 7.48 (+ 1.82) seconds.
% 74.55/10.19 % Length of proof is 378.
% 74.55/10.19 % Level of proof is 114.
% 74.55/10.19 % Maximum clause weight is 18.000.
% 74.55/10.19 % Given clauses 5364.
% 74.55/10.19
% 74.55/10.19 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------