%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : GEO228+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 : n032.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:45 EDT 2024
% Result : Theorem 0.45s 0.55s
% Output : CNFRefutation 0.46s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.05/0.08 % Problem : GEO228+1 : TPTP v8.2.0. Bugfixed v6.4.0.
% 0.05/0.08 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.07/0.27 % Computer : n032.cluster.edu
% 0.07/0.27 % Model : x86_64 x86_64
% 0.07/0.27 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.27 % Memory : 8042.1875MB
% 0.07/0.27 % OS : Linux 3.10.0-693.el7.x86_64
% 0.07/0.27 % CPULimit : 300
% 0.07/0.27 % WCLimit : 300
% 0.07/0.27 % DateTime : Fri Jun 21 08:58:38 EDT 2024
% 0.07/0.27 % CPUTime :
% 0.12/0.45 start to proof:theBenchmark
% 0.45/0.55 %-------------------------------------------
% 0.45/0.55 % File :CSE---1.7
% 0.45/0.55 % Problem :theBenchmark
% 0.45/0.55 % Transform :cnf
% 0.45/0.55 % Format :tptp:raw
% 0.45/0.55 % Command :java -jar mcs_scs.jar %d %s
% 0.45/0.55
% 0.45/0.55 % Result :Theorem 0.050000s
% 0.45/0.55 % Output :CNFRefutation 0.050000s
% 0.45/0.55 %-------------------------------------------
% 0.45/0.55 %------------------------------------------------------------------------------
% 0.45/0.55 % File : GEO228+1 : TPTP v8.2.0. Bugfixed v6.4.0.
% 0.45/0.55 % Domain : Geometry (Constructive)
% 0.45/0.55 % Problem : Obervability of equal or opposite direction
% 0.45/0.55 % Version : [vPl98] axioms : Especial.
% 0.45/0.55 % English :
% 0.45/0.55
% 0.45/0.55 % Refs : [vPl98] von Plato (1998), A Constructive Theory of Ordered Aff
% 0.45/0.55 % : [ROK06] Raths et al. (2006), The ILTP Problem Library for Intu
% 0.45/0.55 % Source : [ILTP]
% 0.45/0.55 % Names : Therorem 3.2 [vPl98]
% 0.45/0.55
% 0.45/0.55 % Status : Theorem
% 0.45/0.55 % Rating : 0.00 v7.3.0, 0.14 v7.2.0, 0.17 v7.1.0, 0.25 v7.0.0, 0.00 v6.4.0
% 0.45/0.55 % Syntax : Number of formulae : 32 ( 7 unt; 0 def)
% 0.45/0.55 % Number of atoms : 105 ( 0 equ)
% 0.45/0.55 % Maximal formula atoms : 10 ( 3 avg)
% 0.45/0.55 % Number of connectives : 92 ( 19 ~; 25 |; 25 &)
% 0.45/0.55 % ( 6 <=>; 17 =>; 0 <=; 0 <~>)
% 0.45/0.55 % Maximal formula depth : 13 ( 6 avg)
% 0.45/0.55 % Maximal term depth : 3 ( 1 avg)
% 0.45/0.55 % Number of predicates : 12 ( 12 usr; 0 prp; 1-4 aty)
% 0.45/0.55 % Number of functors : 4 ( 4 usr; 0 con; 1-2 aty)
% 0.45/0.55 % Number of variables : 73 ( 73 !; 0 ?)
% 0.45/0.55 % SPC : FOF_THM_RFO_NEQ
% 0.45/0.55
% 0.45/0.55 % Comments : Definitions unfolded, hence Especial.
% 0.45/0.55 % Bugfixes : v6.4.0 - Bugfix in GEO007+1.ax
% 0.45/0.55 %------------------------------------------------------------------------------
% 0.45/0.55 include('Axioms/GEO007+0.ax').
% 0.45/0.55 %------------------------------------------------------------------------------
% 0.45/0.55 fof(con,conjecture,
% 0.45/0.55 ! [L,M] :
% 0.45/0.55 ( ~ convergent_lines(L,M)
% 0.45/0.55 <=> ( ~ unequally_directed_lines(L,M)
% 0.45/0.55 | ~ unequally_directed_lines(L,reverse_line(M)) ) ) ).
% 0.45/0.55
% 0.45/0.55 %------------------------------------------------------------------------------
% 0.45/0.55 %-------------------------------------------
% 0.45/0.55 % Proof found
% 0.45/0.55 % SZS status Theorem for theBenchmark
% 0.45/0.55 % SZS output start Proof
% 0.45/0.55 %ClaNum:61(EqnAxiom:0)
% 0.45/0.55 %VarNum:269(SingletonVarNum:105)
% 0.45/0.55 %MaxLitNum:10
% 0.45/0.55 %MaxfuncDepth:2
% 0.45/0.55 %SharedTerms:9
% 0.45/0.55 %goalClause: 13 14 27
% 0.45/0.55 [2]~P9(x21,x21)
% 0.46/0.55 [3]~P2(x31,x31)
% 0.46/0.55 [4]~P3(x41,x41)
% 0.46/0.55 [7]~P3(x71,f1(x71))
% 0.46/0.55 [1]~P1(x11,x12)
% 0.46/0.55 [5]~P10(x51,x52)
% 0.46/0.55 [9]~P4(x91,f2(x92,x91))
% 0.46/0.55 [10]~P9(f2(x101,x102),x101)
% 0.46/0.55 [11]~P9(f3(x111,x112),f1(f3(x112,x111)))
% 0.46/0.55 [13]P5(a4,a5)+P9(a4,a5)
% 0.46/0.55 [14]P5(a4,a5)+P9(a4,f1(a5))
% 0.46/0.55 [12]~P11(x121)+P11(f1(x121))
% 0.46/0.55 [16]~P5(x161,x162)+P9(x161,x162)
% 0.46/0.55 [17]~P5(x171,x172)+P9(x171,f1(x172))
% 0.46/0.55 [32]~P2(x321,x322)+~P4(x322,f3(x321,x322))
% 0.46/0.55 [33]~P2(x331,x332)+~P4(x331,f3(x331,x332))
% 0.46/0.55 [40]P2(x401,x402)+~P6(x403,x401,x402)
% 0.46/0.55 [53]~P6(x531,x532,x533)+~P9(x531,f3(x532,x533))
% 0.46/0.55 [27]~P5(a4,a5)+~P9(a4,a5)+~P9(a4,f1(a5))
% 0.46/0.55 [18]~P11(x181)+~P12(x182)+P11(f2(x181,x182))
% 0.46/0.55 [26]~P4(x261,x262)+P1(x261,x262)+P1(x261,f1(x262))
% 0.46/0.55 [29]~P9(x291,x292)+P5(x291,x292)+~P9(x291,f1(x292))
% 0.46/0.55 [48]~P9(x481,x482)+~P9(x481,f1(x482))+~P4(f6(x481,x482),x482)
% 0.46/0.55 [49]~P9(x491,x492)+~P9(x491,f1(x492))+~P4(f6(x491,x492),x491)
% 0.46/0.55 [22]~P9(x223,x221)+P9(x221,x222)+P9(x223,x222)
% 0.46/0.55 [24]~P2(x243,x241)+P2(x241,x242)+P2(x243,x242)
% 0.46/0.55 [25]~P3(x253,x251)+P3(x251,x252)+P3(x253,x252)
% 0.46/0.55 [45]~P8(x452,x451,x453)+P1(x451,x452)+P1(x453,x452)
% 0.46/0.56 [50]P1(x501,x502)+~P8(x502,x503,x501)+P1(x501,f1(x502))
% 0.46/0.56 [51]P1(x511,x512)+~P8(x512,x511,x513)+P1(x511,f1(x512))
% 0.46/0.56 [52]~P8(x522,x523,x521)+P1(x521,f1(x522))+P1(x523,f1(x522))
% 0.46/0.56 [56]~P6(x561,x563,x562)+~P6(x561,x564,x563)+P7(x561,x562,x563,x564)
% 0.46/0.56 [57]~P6(x571,x573,x574)+~P6(x571,x572,x573)+P7(x571,x572,x573,x574)
% 0.46/0.56 [58]~P7(x581,x582,x583,x584)+P6(x581,x582,x583)+P6(x581,x584,x583)
% 0.46/0.56 [59]P6(x591,x593,x592)+P6(x591,x592,x593)+~P7(x591,x594,x592,x593)
% 0.46/0.56 [60]P6(x601,x603,x602)+P6(x601,x602,x603)+~P7(x601,x602,x603,x604)
% 0.46/0.56 [61]~P7(x611,x614,x612,x613)+P6(x611,x612,x613)+P6(x611,x612,x614)
% 0.46/0.56 [20]~P11(x202)+~P11(x201)+P9(x201,x202)+P9(x201,f1(x202))
% 0.46/0.56 [28]~P12(x282)+~P12(x281)+~P2(x281,x282)+P11(f3(x281,x282))
% 0.46/0.56 [36]~P9(x361,x362)+P10(x361,x362)+P10(x361,f1(x362))+~P9(x361,f1(x362))
% 0.46/0.56 [34]~P9(x341,x343)+P9(x341,x342)+~P9(x341,f1(x343))+P9(x343,f1(x342))
% 0.46/0.56 [35]~P9(x353,x351)+P9(x351,x352)+~P9(x353,f1(x351))+P9(x353,f1(x352))
% 0.46/0.56 [38]~P11(x382)+~P11(x381)+~P9(x381,x382)+~P9(x381,f1(x382))+P12(f6(x381,x382))
% 0.46/0.56 [55]P6(x552,x553,x551)+~P2(x553,x551)+P1(x551,x552)+P1(x553,x552)+P1(x551,f1(x552))+P1(x553,f1(x552))+P9(x552,f3(x553,x551))
% 0.46/0.56 [54]P1(x544,x543)+~P2(x544,x541)+~P3(x543,x542)+P1(x541,x542)+P1(x541,x543)+P1(x544,x542)+P1(x541,f1(x542))+P1(x541,f1(x543))+P1(x544,f1(x542))+P1(x544,f1(x543))
% 0.46/0.56 %EqnAxiom
% 0.46/0.56
% 0.46/0.56 %-------------------------------------------
% 0.46/0.56 cnf(314,plain,
% 0.46/0.56 (P9(a4,a5)),
% 0.46/0.56 inference(scs_inference,[],[13,16])).
% 0.46/0.56 cnf(319,plain,
% 0.46/0.56 (P10(a4,a5)+~P9(a4,f1(a5))),
% 0.46/0.56 inference(scs_inference,[],[314,2,5,22,36])).
% 0.46/0.56 cnf(322,plain,
% 0.46/0.56 (P10(a4,a5)+P5(a4,a5)),
% 0.46/0.56 inference(scs_inference,[],[314,2,5,22,36,14])).
% 0.46/0.56 cnf(343,plain,
% 0.46/0.56 (~P9(a4,f1(a5))),
% 0.46/0.56 inference(scs_inference,[],[5,319])).
% 0.46/0.56 cnf(344,plain,
% 0.46/0.56 (P5(a4,a5)),
% 0.46/0.56 inference(scs_inference,[],[5,322])).
% 0.46/0.56 cnf(360,plain,
% 0.46/0.56 ($false),
% 0.46/0.56 inference(scs_inference,[],[344,343,17]),
% 0.46/0.56 ['proof']).
% 0.46/0.56 % SZS output end Proof
% 0.46/0.56 % Total time :0.050000s
%------------------------------------------------------------------------------