%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : GEO262+1 : TPTP v8.2.0. Bugfixed v6.4.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% Computer : n022.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Mon Jun 24 06:05:00 EDT 2024
% Result : Theorem 1.41s 1.48s
% Output : CNFRefutation 1.41s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.12 % Problem : GEO262+1 : TPTP v8.2.0. Bugfixed v6.4.0.
% 0.04/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.12/0.33 % Computer : n022.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Fri Jun 21 09:39:38 EDT 2024
% 0.12/0.33 % CPUTime :
% 0.19/0.56 start to proof:theBenchmark
% 1.41/1.47 %-------------------------------------------
% 1.41/1.47 % File :CSE---1.7
% 1.41/1.47 % Problem :theBenchmark
% 1.41/1.47 % Transform :cnf
% 1.41/1.47 % Format :tptp:raw
% 1.41/1.47 % Command :java -jar mcs_scs.jar %d %s
% 1.41/1.47
% 1.41/1.47 % Result :Theorem 0.870000s
% 1.41/1.47 % Output :CNFRefutation 0.870000s
% 1.41/1.47 %-------------------------------------------
% 1.41/1.48 %------------------------------------------------------------------------------
% 1.41/1.48 % File : GEO262+1 : TPTP v8.2.0. Bugfixed v6.4.0.
% 1.41/1.48 % Domain : Geometry (Constructive)
% 1.41/1.48 % Problem : Lemma for parallel projection preserves or reverses order
% 1.41/1.48 % Version : [vPl98] axioms : Especial.
% 1.41/1.48 % English :
% 1.41/1.48
% 1.41/1.48 % Refs : [vPl98] von Plato (1998), A Constructive Theory of Ordered Aff
% 1.41/1.48 % : [ROK06] Raths et al. (2006), The ILTP Problem Library for Intu
% 1.41/1.48 % Source : [ILTP]
% 1.41/1.48 % Names : Lemma 6.6 [vPl98]
% 1.41/1.48
% 1.41/1.48 % Status : Theorem
% 1.41/1.48 % Rating : 0.00 v7.5.0, 0.05 v7.4.0, 0.00 v7.0.0, 0.07 v6.4.0
% 1.41/1.48 % Syntax : Number of formulae : 32 ( 7 unt; 0 def)
% 1.41/1.48 % Number of atoms : 109 ( 0 equ)
% 1.41/1.48 % Maximal formula atoms : 10 ( 3 avg)
% 1.41/1.48 % Number of connectives : 95 ( 18 ~; 24 |; 30 &)
% 1.41/1.48 % ( 5 <=>; 18 =>; 0 <=; 0 <~>)
% 1.41/1.48 % Maximal formula depth : 14 ( 6 avg)
% 1.41/1.48 % Maximal term depth : 3 ( 1 avg)
% 1.41/1.48 % Number of predicates : 12 ( 12 usr; 0 prp; 1-4 aty)
% 1.41/1.48 % Number of functors : 4 ( 4 usr; 0 con; 1-2 aty)
% 1.41/1.48 % Number of variables : 77 ( 77 !; 0 ?)
% 1.41/1.48 % SPC : FOF_THM_RFO_NEQ
% 1.41/1.48
% 1.41/1.48 % Comments : Definitions unfolded, hence Especial.
% 1.41/1.48 % Bugfixes : v6.4.0 - Bugfix in GEO007+1.ax
% 1.41/1.48 %------------------------------------------------------------------------------
% 1.41/1.48 include('Axioms/GEO007+0.ax').
% 1.41/1.48 %------------------------------------------------------------------------------
% 1.41/1.48 fof(con,conjecture,
% 1.41/1.48 ! [L,M,N,A,B,C] :
% 1.41/1.48 ( ( between_on_line(L,A,B,C)
% 1.41/1.48 & convergent_lines(L,M)
% 1.41/1.48 & ~ apart_point_and_line(B,M)
% 1.41/1.48 & convergent_lines(L,N)
% 1.41/1.48 & convergent_lines(M,N)
% 1.41/1.48 & ~ apart_point_and_line(B,N) )
% 1.41/1.48 => between_on_line(M,intersection_point(M,parallel_through_point(N,A)),B,intersection_point(M,parallel_through_point(N,C))) ) ).
% 1.41/1.48
% 1.41/1.48 %------------------------------------------------------------------------------
% 1.41/1.48 %-------------------------------------------
% 1.41/1.48 % Proof found
% 1.41/1.48 % SZS status Theorem for theBenchmark
% 1.41/1.48 % SZS output start Proof
% 1.41/1.48 %ClaNum:65(EqnAxiom:0)
% 1.41/1.48 %VarNum:269(SingletonVarNum:105)
% 1.41/1.48 %MaxLitNum:10
% 1.41/1.48 %MaxfuncDepth:2
% 1.41/1.48 %SharedTerms:17
% 1.41/1.48 %goalClause: 1 2 3 4 5 6 18
% 1.41/1.48 %singleGoalClaCount:7
% 1.41/1.48 [1]P1(a1,a2)
% 1.41/1.48 [2]P1(a1,a3)
% 1.41/1.48 [3]P1(a2,a3)
% 1.41/1.48 [4]P2(a1,a4,a5,a6)
% 1.41/1.48 [5]~P3(a5,a2)
% 1.41/1.48 [6]~P3(a5,a3)
% 1.41/1.48 [18]~P2(a2,f10(a2,f8(a3,a4)),a5,f10(a2,f8(a3,a6)))
% 1.41/1.48 [8]~P9(x81,x81)
% 1.41/1.48 [9]~P6(x91,x91)
% 1.41/1.48 [10]~P7(x101,x101)
% 1.41/1.48 [13]~P7(x131,f7(x131))
% 1.41/1.48 [7]~P5(x71,x72)
% 1.41/1.48 [11]~P10(x111,x112)
% 1.41/1.48 [15]~P3(x151,f8(x152,x151))
% 1.41/1.48 [16]~P9(f8(x161,x162),x161)
% 1.41/1.48 [17]~P9(f9(x171,x172),f7(f9(x172,x171)))
% 1.41/1.48 [19]~P11(x191)+P11(f7(x191))
% 1.41/1.48 [21]~P1(x211,x212)+P9(x211,x212)
% 1.41/1.48 [22]~P1(x221,x222)+P9(x221,f7(x222))
% 1.41/1.48 [36]~P6(x361,x362)+~P3(x362,f9(x361,x362))
% 1.41/1.48 [37]~P6(x371,x372)+~P3(x371,f9(x371,x372))
% 1.41/1.48 [44]P6(x441,x442)+~P4(x443,x441,x442)
% 1.41/1.48 [57]~P4(x571,x572,x573)+~P9(x571,f9(x572,x573))
% 1.41/1.48 [23]~P11(x231)+~P12(x232)+P11(f8(x231,x232))
% 1.41/1.48 [31]~P3(x311,x312)+P5(x311,x312)+P5(x311,f7(x312))
% 1.41/1.48 [33]~P9(x331,x332)+P1(x331,x332)+~P9(x331,f7(x332))
% 1.41/1.48 [52]~P9(x521,x522)+~P9(x521,f7(x522))+~P3(f10(x521,x522),x522)
% 1.41/1.48 [53]~P9(x531,x532)+~P9(x531,f7(x532))+~P3(f10(x531,x532),x531)
% 1.41/1.48 [27]~P9(x273,x271)+P9(x271,x272)+P9(x273,x272)
% 1.41/1.48 [29]~P6(x293,x291)+P6(x291,x292)+P6(x293,x292)
% 1.41/1.48 [30]~P7(x303,x301)+P7(x301,x302)+P7(x303,x302)
% 1.41/1.48 [49]~P8(x492,x491,x493)+P5(x491,x492)+P5(x493,x492)
% 1.41/1.48 [54]P5(x541,x542)+~P8(x542,x543,x541)+P5(x541,f7(x542))
% 1.41/1.48 [55]P5(x551,x552)+~P8(x552,x551,x553)+P5(x551,f7(x552))
% 1.41/1.48 [56]~P8(x562,x563,x561)+P5(x561,f7(x562))+P5(x563,f7(x562))
% 1.41/1.48 [60]~P4(x601,x603,x602)+~P4(x601,x604,x603)+P2(x601,x602,x603,x604)
% 1.41/1.48 [61]~P4(x611,x613,x614)+~P4(x611,x612,x613)+P2(x611,x612,x613,x614)
% 1.41/1.48 [62]~P2(x621,x622,x623,x624)+P4(x621,x622,x623)+P4(x621,x624,x623)
% 1.41/1.48 [63]P4(x631,x633,x632)+P4(x631,x632,x633)+~P2(x631,x634,x632,x633)
% 1.41/1.48 [64]P4(x641,x643,x642)+P4(x641,x642,x643)+~P2(x641,x642,x643,x644)
% 1.41/1.48 [65]~P2(x651,x654,x652,x653)+P4(x651,x652,x653)+P4(x651,x652,x654)
% 1.41/1.48 [25]~P11(x252)+~P11(x251)+P9(x251,x252)+P9(x251,f7(x252))
% 1.41/1.48 [32]~P12(x322)+~P12(x321)+~P6(x321,x322)+P11(f9(x321,x322))
% 1.41/1.48 [40]~P9(x401,x402)+P10(x401,x402)+P10(x401,f7(x402))+~P9(x401,f7(x402))
% 1.41/1.48 [38]~P9(x381,x383)+P9(x381,x382)+~P9(x381,f7(x383))+P9(x383,f7(x382))
% 1.41/1.48 [39]~P9(x393,x391)+P9(x391,x392)+~P9(x393,f7(x391))+P9(x393,f7(x392))
% 1.41/1.48 [42]~P11(x422)+~P11(x421)+~P9(x421,x422)+~P9(x421,f7(x422))+P12(f10(x421,x422))
% 1.41/1.48 [59]P4(x592,x593,x591)+~P6(x593,x591)+P5(x591,x592)+P5(x593,x592)+P5(x591,f7(x592))+P5(x593,f7(x592))+P9(x592,f9(x593,x591))
% 1.41/1.48 [58]P5(x584,x583)+~P6(x584,x581)+~P7(x583,x582)+P5(x581,x582)+P5(x581,x583)+P5(x584,x582)+P5(x581,f7(x582))+P5(x581,f7(x583))+P5(x584,f7(x582))+P5(x584,f7(x583))
% 1.41/1.48 %EqnAxiom
% 1.41/1.48
% 1.41/1.48 %-------------------------------------------
% 1.41/1.48 cnf(93,plain,
% 1.41/1.48 (~P9(f8(x931,x932),x931)),
% 1.41/1.48 inference(rename_variables,[],[16])).
% 1.41/1.48 cnf(97,plain,
% 1.41/1.48 (~P9(x971,f8(x971,x972))),
% 1.41/1.48 inference(scs_inference,[],[16,93,8,22,21,27])).
% 1.41/1.48 cnf(112,plain,
% 1.41/1.48 (~P9(x1121,f8(f8(x1121,x1122),x1123))),
% 1.41/1.48 inference(scs_inference,[],[16,17,97,21,22,27])).
% 1.41/1.48 cnf(127,plain,
% 1.41/1.48 (~P9(x1271,f8(f8(f8(x1271,x1272),x1273),x1274))),
% 1.41/1.48 inference(scs_inference,[],[16,112,21,27])).
% 1.41/1.48 cnf(3419,plain,
% 1.41/1.48 (P9(a3,a1)),
% 1.41/1.48 inference(scs_inference,[],[2,8,21,27])).
% 1.41/1.49 cnf(3420,plain,
% 1.41/1.49 (P9(a1,a3)),
% 1.41/1.49 inference(scs_inference,[],[8,3419,27])).
% 1.41/1.49 cnf(3433,plain,
% 1.41/1.49 (P9(a3,f8(f8(f8(a1,x34331),x34332),x34333))),
% 1.41/1.49 inference(scs_inference,[],[127,3420,27])).
% 1.41/1.49 cnf(3436,plain,
% 1.41/1.49 (P10(a1,a3)+~P9(a1,f7(a3))),
% 1.41/1.49 inference(scs_inference,[],[127,3420,11,27,40])).
% 1.41/1.49 cnf(3447,plain,
% 1.41/1.49 (P9(f8(f8(f8(a1,x34471),x34472),x34473),a3)),
% 1.41/1.49 inference(scs_inference,[],[8,3433,27])).
% 1.41/1.49 cnf(3454,plain,
% 1.41/1.49 (~P9(a1,f7(a3))),
% 1.41/1.49 inference(scs_inference,[],[11,3436])).
% 1.41/1.49 cnf(3459,plain,
% 1.41/1.49 (P10(f8(f8(f8(a1,x34591),x34592),x34593),a3)+~P9(f8(f8(f8(a1,x34591),x34592),x34593),f7(a3))),
% 1.41/1.49 inference(scs_inference,[],[16,3447,11,27,40])).
% 1.41/1.49 cnf(3462,plain,
% 1.41/1.49 (P10(f8(f8(f8(a1,x34621),x34622),x34623),a3)+~P1(f8(f8(f8(a1,x34621),x34622),x34623),a3)),
% 1.41/1.49 inference(scs_inference,[],[16,3447,11,27,40,22])).
% 1.41/1.49 cnf(3464,plain,
% 1.41/1.49 (P10(f8(f8(f8(a1,x34641),x34642),x34643),a3)+~P1(f8(f8(f8(a1,x34641),x34642),x34643),f7(a3))),
% 1.41/1.49 inference(scs_inference,[],[16,3447,11,27,40,22,21])).
% 1.41/1.49 cnf(3470,plain,
% 1.41/1.49 (~P10(x34701,x34702)),
% 1.41/1.49 inference(rename_variables,[],[11])).
% 1.41/1.49 cnf(3472,plain,
% 1.41/1.49 (~P10(x34721,x34722)),
% 1.41/1.49 inference(rename_variables,[],[11])).
% 1.41/1.49 cnf(3475,plain,
% 1.41/1.49 ($false),
% 1.41/1.49 inference(scs_inference,[],[2,3454,11,3470,3472,3464,3462,3459,22]),
% 1.41/1.49 ['proof']).
% 1.41/1.49 % SZS output end Proof
% 1.41/1.49 % Total time :0.870000s
%------------------------------------------------------------------------------