%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : GEO221+2 : TPTP v8.2.0. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% Computer : n001.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:41 EDT 2024
% Result : Theorem 5.77s 5.89s
% Output : CNFRefutation 5.77s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.11 % Problem : GEO221+2 : TPTP v8.2.0. Released v3.3.0.
% 0.03/0.11 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.10/0.31 % Computer : n001.cluster.edu
% 0.10/0.31 % Model : x86_64 x86_64
% 0.10/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.31 % Memory : 8042.1875MB
% 0.10/0.31 % OS : Linux 3.10.0-693.el7.x86_64
% 0.10/0.31 % CPULimit : 300
% 0.10/0.31 % WCLimit : 300
% 0.10/0.31 % DateTime : Fri Jun 21 09:55:24 EDT 2024
% 0.10/0.31 % CPUTime :
% 0.48/0.56 start to proof:theBenchmark
% 5.77/5.88 %-------------------------------------------
% 5.77/5.88 % File :CSE---1.7
% 5.77/5.88 % Problem :theBenchmark
% 5.77/5.88 % Transform :cnf
% 5.77/5.88 % Format :tptp:raw
% 5.77/5.88 % Command :java -jar mcs_scs.jar %d %s
% 5.77/5.88
% 5.77/5.88 % Result :Theorem 5.270000s
% 5.77/5.88 % Output :CNFRefutation 5.270000s
% 5.77/5.88 %-------------------------------------------
% 5.77/5.89 %------------------------------------------------------------------------------
% 5.77/5.89 % File : GEO221+2 : TPTP v8.2.0. Released v3.3.0.
% 5.77/5.89 % Domain : Geometry (Constructive)
% 5.77/5.89 % Problem : Lemma on orthogonality
% 5.77/5.89 % Version : [vPl95] axioms : Reduced > Especial.
% 5.77/5.89 % English : If a point B is incident with the orthogonal to a line L
% 5.77/5.89 % through point A, then this orthogonal is equal to the
% 5.77/5.89 % orthogonal to L through B.
% 5.77/5.89
% 5.77/5.89 % Refs : [vPl95] von Plato (1995), The Axioms of Constructive Geometry
% 5.77/5.89 % : [Li97] Li (1997), Replacing the Axioms for Connecting Lines a
% 5.77/5.89 % : [Li98] Li (1998), A Shorter and Intuitive Axiom to Replace th
% 5.77/5.89 % : [ROK06] Raths et al. (2006), The ILTP Problem Library for Intu
% 5.77/5.89 % Source : [ILTP]
% 5.77/5.89 % Names :
% 5.77/5.89
% 5.77/5.89 % Status : Theorem
% 5.77/5.89 % Rating : 0.00 v7.5.0, 0.05 v7.4.0, 0.00 v7.0.0, 0.07 v6.4.0, 0.00 v6.1.0, 0.16 v6.0.0, 0.25 v5.5.0, 0.17 v5.4.0, 0.13 v5.3.0, 0.17 v5.2.0, 0.21 v5.0.0, 0.10 v4.1.0, 0.11 v4.0.1, 0.16 v4.0.0, 0.20 v3.7.0, 0.14 v3.5.0, 0.00 v3.3.0
% 5.77/5.89 % Syntax : Number of formulae : 21 ( 7 unt; 0 def)
% 5.77/5.89 % Number of atoms : 57 ( 0 equ)
% 5.77/5.89 % Maximal formula atoms : 6 ( 2 avg)
% 5.77/5.89 % Number of connectives : 45 ( 9 ~; 16 |; 5 &)
% 5.77/5.89 % ( 0 <=>; 15 =>; 0 <=; 0 <~>)
% 5.77/5.89 % Maximal formula depth : 9 ( 5 avg)
% 5.77/5.89 % Maximal term depth : 2 ( 1 avg)
% 5.77/5.89 % Number of predicates : 5 ( 5 usr; 0 prp; 2-2 aty)
% 5.77/5.89 % Number of functors : 4 ( 4 usr; 0 con; 2-2 aty)
% 5.77/5.89 % Number of variables : 53 ( 53 !; 0 ?)
% 5.77/5.89 % SPC : FOF_THM_RFO_NEQ
% 5.77/5.89
% 5.77/5.89 % Comments : Definitions unfolded, hence Especial.
% 5.77/5.89 %------------------------------------------------------------------------------
% 5.77/5.89 include('Axioms/GEO008+0.ax').
% 5.77/5.89 include('Axioms/GEO006+2.ax').
% 5.77/5.89 include('Axioms/GEO006+3.ax').
% 5.77/5.89 %------------------------------------------------------------------------------
% 5.77/5.89 fof(con,conjecture,
% 5.77/5.89 ! [A,B,L] :
% 5.77/5.89 ( ~ apart_point_and_line(B,orthogonal_through_point(L,A))
% 5.77/5.89 => ~ distinct_lines(orthogonal_through_point(L,A),orthogonal_through_point(L,B)) ) ).
% 5.77/5.89
% 5.77/5.89 %------------------------------------------------------------------------------
% 5.77/5.89 %-------------------------------------------
% 5.77/5.89 % Proof found
% 5.77/5.89 % SZS status Theorem for theBenchmark
% 5.77/5.89 % SZS output start Proof
% 5.77/5.89 %ClaNum:27(EqnAxiom:0)
% 5.77/5.89 %VarNum:138(SingletonVarNum:62)
% 5.77/5.89 %MaxLitNum:6
% 5.77/5.89 %MaxfuncDepth:1
% 5.77/5.89 %SharedTerms:7
% 5.77/5.89 %goalClause: 1 5
% 5.77/5.89 %singleGoalClaCount:2
% 5.77/5.89 [1]P1(f4(a1,a2),f4(a1,a3))
% 5.77/5.89 [5]~P3(a3,f4(a1,a2))
% 5.77/5.89 [2]~P4(x21,x21)
% 5.77/5.89 [3]~P1(x31,x31)
% 5.77/5.89 [4]~P2(x41,x41)
% 5.77/5.89 [6]~P3(x61,f7(x62,x61))
% 5.77/5.89 [7]~P3(x71,f4(x72,x71))
% 5.77/5.89 [8]~P2(f7(x81,x82),x81)
% 5.77/5.89 [9]~P5(f4(x91,x92),x91)
% 5.77/5.89 [10]P5(x101,x102)+P2(x101,x102)
% 5.77/5.89 [11]~P2(x111,x112)+P1(x111,x112)
% 5.77/5.89 [12]~P4(x123,x121)+P4(x121,x122)+P4(x123,x122)
% 5.77/5.89 [13]~P3(x131,x133)+P4(x131,x132)+P3(x132,x133)
% 5.77/5.89 [14]~P1(x143,x141)+P1(x141,x142)+P1(x143,x142)
% 5.77/5.89 [15]~P3(x153,x151)+P1(x151,x152)+P3(x153,x152)
% 5.77/5.89 [16]~P2(x163,x161)+P2(x161,x162)+P2(x163,x162)
% 5.77/5.89 [23]~P2(x232,x233)+~P3(x231,x233)+P4(x231,f5(x232,x233))
% 5.77/5.89 [24]~P2(x242,x243)+~P3(x241,x242)+P4(x241,f5(x242,x243))
% 5.77/5.89 [25]P4(x251,x252)+~P4(x253,x252)+~P3(x251,f6(x253,x252))
% 5.77/5.89 [26]P4(x261,x262)+~P4(x262,x263)+~P3(x261,f6(x262,x263))
% 5.77/5.89 [17]P3(x173,x171)+~P1(x171,x172)+P2(x171,x172)+P3(x173,x172)
% 5.77/5.89 [19]~P2(x191,x193)+~P5(x191,x193)+P2(x191,x192)+P5(x193,x192)
% 5.77/5.89 [20]~P2(x203,x201)+~P5(x203,x201)+P2(x201,x202)+P5(x203,x202)
% 5.77/5.89 [21]~P2(x211,x213)+~P5(x211,x213)+P5(x211,x212)+P5(x213,x212)
% 5.77/5.89 [22]P5(x223,x224)+~P1(x223,x222)+P3(x221,x222)+P3(x221,x223)+P5(x222,x224)
% 5.77/5.89 [27]P3(x274,x273)+~P4(x274,x271)+~P1(x273,x272)+P3(x271,x272)+P3(x271,x273)+P3(x274,x272)
% 5.77/5.89 %EqnAxiom
% 5.77/5.89
% 5.77/5.89 %-------------------------------------------
% 5.77/5.90 cnf(86,plain,
% 5.77/5.90 (~P2(x861,f7(x861,x862))),
% 5.77/5.90 inference(scs_inference,[],[8,4,16])).
% 5.77/5.90 cnf(94,plain,
% 5.77/5.90 (P1(f4(a1,a3),f7(f4(a1,a2),a3))),
% 5.77/5.90 inference(scs_inference,[],[6,5,1,8,4,16,17,10,14])).
% 5.77/5.90 cnf(612,plain,
% 5.77/5.90 (P5(a1,f4(a1,a2))+~P2(f7(f4(a1,a2),a3),a1)),
% 5.77/5.90 inference(scs_inference,[],[94,8,6,7,3,9,14,22,19])).
% 5.77/5.90 cnf(910,plain,
% 5.77/5.90 (P2(x9101,f7(f4(x9101,x9102),x9103))),
% 5.77/5.90 inference(scs_inference,[],[9,86,10,16])).
% 5.77/5.90 cnf(911,plain,
% 5.77/5.90 (P2(f7(f4(x9111,x9112),x9113),f7(x9111,x9114))),
% 5.77/5.90 inference(scs_inference,[],[86,910,16])).
% 5.77/5.90 cnf(917,plain,
% 5.77/5.90 (P2(f7(x9171,x9172),f4(x9171,x9173))),
% 5.77/5.90 inference(scs_inference,[],[8,911,16])).
% 5.77/5.90 cnf(924,plain,
% 5.77/5.90 (~P4(x9241,x9241)),
% 5.77/5.90 inference(rename_variables,[],[2])).
% 5.77/5.90 cnf(929,plain,
% 5.77/5.90 (P2(f4(x9291,x9292),x9291)),
% 5.77/5.90 inference(scs_inference,[],[2,924,8,917,23,24,16])).
% 5.77/5.90 cnf(935,plain,
% 5.77/5.90 (P2(x9351,f4(x9351,x9352))),
% 5.77/5.90 inference(scs_inference,[],[4,929,16])).
% 5.77/5.90 cnf(1683,plain,
% 5.77/5.90 (P2(f7(x16831,x16832),f7(f4(x16831,x16833),x16834))),
% 5.77/5.90 inference(scs_inference,[],[4,911,16])).
% 5.77/5.90 cnf(1689,plain,
% 5.77/5.90 (P2(f7(f4(x16891,x16892),x16893),x16891)),
% 5.77/5.90 inference(scs_inference,[],[8,1683,16])).
% 5.77/5.90 cnf(1700,plain,
% 5.77/5.90 (P5(a1,f4(a1,a2))),
% 5.77/5.90 inference(scs_inference,[],[1689,612])).
% 5.77/5.90 cnf(1705,plain,
% 5.77/5.90 ($false),
% 5.77/5.90 inference(scs_inference,[],[4,935,1700,9,19]),
% 5.77/5.90 ['proof']).
% 5.77/5.90 % SZS output end Proof
% 5.77/5.90 % Total time :5.270000s
%------------------------------------------------------------------------------