%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : GEO212+2 : TPTP v8.2.0. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% Computer : n021.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:04:35 EDT 2024
% Result : Theorem 12.58s 12.64s
% Output : CNFRefutation 12.58s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : GEO212+2 : TPTP v8.2.0. Released v3.3.0.
% 0.06/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.12/0.33 % Computer : n021.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 07:51:24 EDT 2024
% 0.12/0.33 % CPUTime :
% 0.19/0.55 start to proof:theBenchmark
% 12.58/12.64 %-------------------------------------------
% 12.58/12.64 % File :CSE---1.7
% 12.58/12.64 % Problem :theBenchmark
% 12.58/12.64 % Transform :cnf
% 12.58/12.64 % Format :tptp:raw
% 12.58/12.64 % Command :java -jar mcs_scs.jar %d %s
% 12.58/12.64
% 12.58/12.64 % Result :Theorem 12.040000s
% 12.58/12.64 % Output :CNFRefutation 12.040000s
% 12.58/12.64 %-------------------------------------------
% 12.58/12.64 %------------------------------------------------------------------------------
% 12.58/12.64 % File : GEO212+2 : TPTP v8.2.0. Released v3.3.0.
% 12.58/12.64 % Domain : Geometry (Constructive)
% 12.58/12.64 % Problem : Non-orthogonal lines and a third line
% 12.58/12.64 % Version : [vPl95] axioms : Reduced > Especial.
% 12.58/12.64 % English : If a line L is not orthogonal to M, then a third line N is
% 12.58/12.64 % convergent to L or not orthogonal to M.
% 12.58/12.64
% 12.58/12.64 % Refs : [vPl95] von Plato (1995), The Axioms of Constructive Geometry
% 12.58/12.64 % : [Li97] Li (1997), Replacing the Axioms for Connecting Lines a
% 12.58/12.64 % : [Li98] Li (1998), A Shorter and Intuitive Axiom to Replace th
% 12.58/12.64 % : [ROK06] Raths et al. (2006), The ILTP Problem Library for Intu
% 12.58/12.64 % Source : [ILTP]
% 12.58/12.64 % Names :
% 12.58/12.64
% 12.58/12.64 % Status : Theorem
% 12.58/12.64 % Rating : 0.06 v8.2.0, 0.00 v6.1.0, 0.04 v6.0.0, 0.25 v5.5.0, 0.08 v5.4.0, 0.13 v5.2.0, 0.14 v5.0.0, 0.05 v4.1.0, 0.06 v4.0.1, 0.05 v3.7.0, 0.00 v3.3.0
% 12.58/12.64 % Syntax : Number of formulae : 21 ( 7 unt; 0 def)
% 12.58/12.64 % Number of atoms : 58 ( 0 equ)
% 12.58/12.64 % Maximal formula atoms : 6 ( 2 avg)
% 12.58/12.64 % Number of connectives : 44 ( 7 ~; 17 |; 5 &)
% 12.58/12.64 % ( 0 <=>; 15 =>; 0 <=; 0 <~>)
% 12.58/12.64 % Maximal formula depth : 9 ( 5 avg)
% 12.58/12.64 % Maximal term depth : 2 ( 1 avg)
% 12.58/12.64 % Number of predicates : 5 ( 5 usr; 0 prp; 2-2 aty)
% 12.58/12.64 % Number of functors : 4 ( 4 usr; 0 con; 2-2 aty)
% 12.58/12.64 % Number of variables : 53 ( 53 !; 0 ?)
% 12.58/12.64 % SPC : FOF_THM_RFO_NEQ
% 12.58/12.64
% 12.58/12.64 % Comments : Definitions unfolded, hence Especial.
% 12.58/12.64 %------------------------------------------------------------------------------
% 12.58/12.64 include('Axioms/GEO008+0.ax').
% 12.58/12.64 include('Axioms/GEO006+2.ax').
% 12.58/12.64 include('Axioms/GEO006+3.ax').
% 12.58/12.64 %------------------------------------------------------------------------------
% 12.58/12.64 fof(con,conjecture,
% 12.58/12.64 ! [L,M,N] :
% 12.58/12.64 ( unorthogonal_lines(L,M)
% 12.58/12.64 => ( convergent_lines(L,N)
% 12.58/12.64 | unorthogonal_lines(M,N) ) ) ).
% 12.58/12.64
% 12.58/12.64 %------------------------------------------------------------------------------
% 12.58/12.64 %-------------------------------------------
% 12.58/12.64 % Proof found
% 12.58/12.64 % SZS status Theorem for theBenchmark
% 12.58/12.64 % SZS output start Proof
% 12.58/12.65 %ClaNum:28(EqnAxiom:0)
% 12.58/12.65 %VarNum:138(SingletonVarNum:62)
% 12.58/12.65 %MaxLitNum:6
% 12.58/12.65 %MaxfuncDepth:1
% 12.58/12.65 %SharedTerms:6
% 12.58/12.65 %goalClause: 1 2 3
% 12.58/12.65 %singleGoalClaCount:3
% 12.58/12.65 [1]P1(a1,a2)
% 12.58/12.65 [2]~P2(a1,a3)
% 12.58/12.65 [3]~P1(a2,a3)
% 12.58/12.65 [4]~P4(x41,x41)
% 12.58/12.65 [5]~P5(x51,x51)
% 12.58/12.65 [6]~P2(x61,x61)
% 12.58/12.65 [7]~P3(x71,f4(x72,x71))
% 12.58/12.65 [8]~P3(x81,f5(x82,x81))
% 12.58/12.65 [9]~P2(f4(x91,x92),x91)
% 12.58/12.65 [10]~P1(f5(x101,x102),x101)
% 12.58/12.65 [11]P1(x111,x112)+P2(x111,x112)
% 12.58/12.65 [12]~P2(x121,x122)+P5(x121,x122)
% 12.58/12.65 [13]~P4(x133,x131)+P4(x131,x132)+P4(x133,x132)
% 12.58/12.65 [14]~P3(x141,x143)+P4(x141,x142)+P3(x142,x143)
% 12.58/12.65 [15]~P5(x153,x151)+P5(x151,x152)+P5(x153,x152)
% 12.58/12.65 [16]~P3(x163,x161)+P5(x161,x162)+P3(x163,x162)
% 12.58/12.65 [17]~P2(x173,x171)+P2(x171,x172)+P2(x173,x172)
% 12.58/12.65 [24]~P2(x242,x243)+~P3(x241,x243)+P4(x241,f6(x242,x243))
% 12.58/12.65 [25]~P2(x252,x253)+~P3(x251,x252)+P4(x251,f6(x252,x253))
% 12.58/12.65 [26]P4(x261,x262)+~P4(x263,x262)+~P3(x261,f7(x263,x262))
% 12.58/12.65 [27]P4(x271,x272)+~P4(x272,x273)+~P3(x271,f7(x272,x273))
% 12.58/12.65 [18]P3(x183,x181)+~P5(x181,x182)+P2(x181,x182)+P3(x183,x182)
% 12.58/12.65 [20]~P2(x201,x203)+~P1(x201,x203)+P2(x201,x202)+P1(x203,x202)
% 12.58/12.65 [21]~P2(x213,x211)+~P1(x213,x211)+P2(x211,x212)+P1(x213,x212)
% 12.58/12.65 [22]~P2(x221,x223)+~P1(x221,x223)+P1(x221,x222)+P1(x223,x222)
% 12.58/12.65 [23]P1(x233,x234)+~P5(x233,x232)+P3(x231,x232)+P3(x231,x233)+P1(x232,x234)
% 12.58/12.65 [28]P3(x284,x283)+~P4(x284,x281)+~P5(x283,x282)+P3(x281,x282)+P3(x281,x283)+P3(x284,x282)
% 12.58/12.65 %EqnAxiom
% 12.58/12.65
% 12.58/12.65 %-------------------------------------------
% 12.58/12.65 cnf(29,plain,
% 12.58/12.65 (P1(a1,a3)),
% 12.58/12.65 inference(scs_inference,[],[2,11])).
% 12.58/12.65 cnf(31,plain,
% 12.58/12.65 (~P2(a3,a1)),
% 12.58/12.65 inference(scs_inference,[],[2,6,11,17])).
% 12.58/12.65 cnf(34,plain,
% 12.58/12.65 (~P2(a1,a2)),
% 12.58/12.65 inference(scs_inference,[],[1,2,3,6,11,17,20])).
% 12.58/12.65 cnf(36,plain,
% 12.58/12.65 (~P2(x361,x362)+~P3(f6(x361,x362),x362)),
% 12.58/12.65 inference(scs_inference,[],[1,2,3,6,4,11,17,20,24])).
% 12.58/12.65 cnf(37,plain,
% 12.58/12.65 (~P4(x371,x371)),
% 12.58/12.65 inference(rename_variables,[],[4])).
% 12.58/12.65 cnf(39,plain,
% 12.58/12.65 (~P2(x391,x392)+~P3(f6(x391,x392),x391)),
% 12.58/12.65 inference(scs_inference,[],[1,2,3,6,4,37,11,17,20,24,25])).
% 12.58/12.65 cnf(45,plain,
% 12.58/12.65 (~P2(a2,a1)),
% 12.58/12.65 inference(scs_inference,[],[34,31,6,11,17])).
% 12.58/12.65 cnf(59,plain,
% 12.58/12.65 (~P2(f4(a2,x591),a1)),
% 12.58/12.65 inference(scs_inference,[],[34,45,9,11,17])).
% 12.58/12.65 cnf(60,plain,
% 12.58/12.65 (~P2(f4(x601,x602),x601)),
% 12.58/12.65 inference(rename_variables,[],[9])).
% 12.58/12.65 cnf(62,plain,
% 12.58/12.65 (~P5(f4(f5(x621,x622),x622),f5(x621,x622))),
% 12.58/12.65 inference(scs_inference,[],[34,45,9,60,8,7,11,17,18])).
% 12.58/12.65 cnf(81,plain,
% 12.58/12.65 (~P2(f5(x811,x812),f4(f5(x811,x812),x812))),
% 12.58/12.65 inference(scs_inference,[],[62,59,5,11,15,12])).
% 12.58/12.65 cnf(100,plain,
% 12.58/12.65 (P1(f4(x1001,x1002),a3)+~P5(f4(x1001,x1002),a2)+P3(x1002,a2)),
% 12.58/12.65 inference(scs_inference,[],[34,3,29,6,7,11,23])).
% 12.58/12.65 cnf(106,plain,
% 12.58/12.65 (~P2(f4(a3,x1061),a1)),
% 12.58/12.65 inference(scs_inference,[],[2,9,81,11,17])).
% 12.58/12.65 cnf(898,plain,
% 12.58/12.65 (P3(x8981,a3)+P3(x8981,a1)+~P5(a1,a3)),
% 12.58/12.65 inference(scs_inference,[],[2,29,18])).
% 12.58/12.65 cnf(922,plain,
% 12.58/12.65 (~P2(x9221,a1)+P3(f6(x9221,a1),a3)+~P5(a1,a3)),
% 12.58/12.65 inference(scs_inference,[],[898,36])).
% 12.58/12.65 cnf(938,plain,
% 12.58/12.65 (P3(f6(f5(a1,x9381),a1),a3)+~P5(a1,a3)),
% 12.58/12.65 inference(scs_inference,[],[10,922,11])).
% 12.58/12.65 cnf(1130,plain,
% 12.58/12.65 (P5(a2,a3)),
% 12.58/12.65 inference(scs_inference,[],[3,11,12])).
% 12.58/12.65 cnf(1131,plain,
% 12.58/12.65 (P5(a3,a2)),
% 12.58/12.65 inference(scs_inference,[],[1130,5,15])).
% 12.58/12.65 cnf(1149,plain,
% 12.58/12.65 (~P3(f6(a2,a3),a3)),
% 12.58/12.65 inference(scs_inference,[],[3,11,36])).
% 12.58/12.65 cnf(1150,plain,
% 12.58/12.66 (P3(f6(a2,a3),a1)+~P5(a1,a3)),
% 12.58/12.66 inference(scs_inference,[],[2,1149,18])).
% 12.58/12.66 cnf(1153,plain,
% 12.58/12.66 (P3(f6(a2,a3),a1)+~P5(a3,a1)),
% 12.58/12.66 inference(scs_inference,[],[31,1149,18])).
% 12.58/12.66 cnf(1185,plain,
% 12.58/12.66 (P5(a1,f5(x11851,f6(a2,a3)))+~P5(a3,a1)),
% 12.58/12.66 inference(scs_inference,[],[8,1153,16])).
% 12.58/12.66 cnf(1217,plain,
% 12.58/12.66 (P5(a2,a1)+P5(a1,f5(x12171,f6(a2,a3)))),
% 12.58/12.66 inference(scs_inference,[],[1131,1185,15])).
% 12.58/12.66 cnf(1233,plain,
% 12.58/12.66 (P5(f5(x12331,f6(a2,a3)),a1)+P5(a2,a1)),
% 12.58/12.66 inference(scs_inference,[],[5,1217,15])).
% 12.58/12.66 cnf(1249,plain,
% 12.58/12.66 (P2(f5(x12491,f6(a2,a3)),a1)+P3(f6(a2,a3),a1)+P5(a2,a1)),
% 12.58/12.66 inference(scs_inference,[],[8,1233,18])).
% 12.58/12.66 cnf(1260,plain,
% 12.58/12.66 (~P2(x12601,f4(x12601,x12602))),
% 12.58/12.66 inference(scs_inference,[],[9,6,17])).
% 12.58/12.66 cnf(1261,plain,
% 12.58/12.66 (~P2(x12611,x12611)),
% 12.58/12.66 inference(rename_variables,[],[6])).
% 12.58/12.66 cnf(1273,plain,
% 12.58/12.66 (~P2(a3,a2)+~P5(f5(a2,f6(a2,a3)),a3)),
% 12.58/12.66 inference(scs_inference,[],[9,3,6,1261,1149,7,8,10,17,18,11,23,20])).
% 12.58/12.66 cnf(1283,plain,
% 12.58/12.66 (~P5(a3,f4(a3,f6(a2,a3)))),
% 12.58/12.66 inference(scs_inference,[],[9,1260,1149,7,11,17,18])).
% 12.58/12.66 cnf(1336,plain,
% 12.58/12.66 (P3(f6(a2,a3),a2)+~P5(f5(a2,f6(a2,a3)),a3)),
% 12.58/12.66 inference(scs_inference,[],[1131,1149,1273,18])).
% 12.58/12.66 cnf(1460,plain,
% 12.58/12.66 (~P2(a2,a3)+~P5(f5(a2,f6(a2,a3)),a3)),
% 12.58/12.66 inference(scs_inference,[],[1336,39])).
% 12.58/12.66 cnf(1491,plain,
% 12.58/12.66 (~P5(f5(a2,f6(a2,a3)),a3)),
% 12.58/12.66 inference(scs_inference,[],[3,1460,11])).
% 12.58/12.66 cnf(1492,plain,
% 12.58/12.66 (~P2(f5(a2,f6(a2,a3)),a3)),
% 12.58/12.66 inference(scs_inference,[],[1491,12])).
% 12.58/12.66 cnf(1769,plain,
% 12.58/12.66 (~P3(f6(a2,a3),a2)),
% 12.58/12.66 inference(scs_inference,[],[3,11,39])).
% 12.58/12.66 cnf(1791,plain,
% 12.58/12.66 (P3(f6(a2,a3),a1)+P2(a1,f5(x17911,f6(a2,a3)))),
% 12.58/12.66 inference(scs_inference,[],[6,45,1491,1769,18,1217,1233,1249,100,15,17])).
% 12.58/12.66 cnf(2443,plain,
% 12.58/12.66 (P5(a1,a3)+P2(a1,f5(x24431,f6(a2,a3)))),
% 12.58/12.66 inference(scs_inference,[],[1149,1791,16])).
% 12.58/12.66 cnf(2474,plain,
% 12.58/12.66 (P2(a1,f5(x24741,f6(a2,a3)))+P3(f6(f5(a1,x24742),a1),a3)),
% 12.58/12.66 inference(scs_inference,[],[2443,938])).
% 12.58/12.66 cnf(2705,plain,
% 12.58/12.66 (P3(f6(f5(a1,x27051),a1),a3)),
% 12.58/12.66 inference(scs_inference,[],[2,1492,2474,17])).
% 12.58/12.66 cnf(3392,plain,
% 12.58/12.66 (~P2(f4(a1,x33921),f4(a2,x33922))),
% 12.58/12.66 inference(scs_inference,[],[59,9,17])).
% 12.58/12.66 cnf(3956,plain,
% 12.58/12.66 (~P2(f5(a1,x39561),a1)+P5(a3,a1)),
% 12.58/12.66 inference(scs_inference,[],[2705,36,16])).
% 12.58/12.66 cnf(3987,plain,
% 12.58/12.66 (P3(f6(a2,a3),a1)+~P2(f5(a1,x39871),a1)),
% 12.58/12.66 inference(scs_inference,[],[3956,1153])).
% 12.58/12.66 cnf(4021,plain,
% 12.58/12.66 (P5(a1,a3)+~P2(f5(a1,x40211),a1)),
% 12.58/12.66 inference(scs_inference,[],[1149,3987,16])).
% 12.58/12.66 cnf(4059,plain,
% 12.58/12.66 (P5(a1,a3)),
% 12.58/12.66 inference(scs_inference,[],[10,4021,11])).
% 12.58/12.66 cnf(4063,plain,
% 12.58/12.66 (P3(f6(a2,a3),a1)),
% 12.58/12.66 inference(scs_inference,[],[4059,1150])).
% 12.58/12.66 cnf(4082,plain,
% 12.58/12.66 (P5(a3,f4(a1,f6(a2,a3)))),
% 12.58/12.66 inference(scs_inference,[],[3392,1260,4063,1130,7,1769,16,17,18,11,15])).
% 12.58/12.66 cnf(4903,plain,
% 12.58/12.66 (P3(x49031,f4(a1,x49032))+~P5(f4(a1,x49032),f4(a3,x49031))),
% 12.58/12.66 inference(scs_inference,[],[106,9,7,17,11,18])).
% 12.58/12.66 cnf(4916,plain,
% 12.58/12.66 (~P5(f4(a1,x49161),f4(a3,x49161))),
% 12.58/12.66 inference(scs_inference,[],[7,4,4903,14])).
% 12.58/12.66 cnf(4917,plain,
% 12.58/12.66 ($false),
% 12.58/12.66 inference(scs_inference,[],[1283,4916,4082,15]),
% 12.58/12.66 ['proof']).
% 12.58/12.66 % SZS output end Proof
% 12.58/12.66 % Total time :12.040000s
%------------------------------------------------------------------------------