%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : GEO215+1 : TPTP v8.1.0. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n026.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 : 0s
% DateTime : Sat Jul 16 02:52:51 EDT 2022
% Result : Theorem 1.48s 1.87s
% Output : Refutation 1.48s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : GEO215+1 : TPTP v8.1.0. Released v3.3.0.
% 0.03/0.13 % Command : bliksem %s
% 0.13/0.34 % Computer : n026.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % DateTime : Sat Jun 18 00:51:24 EDT 2022
% 0.13/0.34 % CPUTime :
% 1.48/1.87 *** allocated 10000 integers for termspace/termends
% 1.48/1.87 *** allocated 10000 integers for clauses
% 1.48/1.87 *** allocated 10000 integers for justifications
% 1.48/1.87 Bliksem 1.12
% 1.48/1.87
% 1.48/1.87
% 1.48/1.87 Automatic Strategy Selection
% 1.48/1.87
% 1.48/1.87
% 1.48/1.87 Clauses:
% 1.48/1.87
% 1.48/1.87 { ! distinct_points( X, X ) }.
% 1.48/1.87 { ! distinct_lines( X, X ) }.
% 1.48/1.87 { ! convergent_lines( X, X ) }.
% 1.48/1.87 { ! distinct_points( X, Y ), distinct_points( X, Z ), distinct_points( Y, Z
% 1.48/1.87 ) }.
% 1.48/1.87 { ! distinct_lines( X, Y ), distinct_lines( X, Z ), distinct_lines( Y, Z )
% 1.48/1.87 }.
% 1.48/1.87 { ! convergent_lines( X, Y ), convergent_lines( X, Z ), convergent_lines( Y
% 1.48/1.87 , Z ) }.
% 1.48/1.87 { ! distinct_points( X, Y ), ! apart_point_and_line( X, line_connecting( X
% 1.48/1.87 , Y ) ) }.
% 1.48/1.87 { ! distinct_points( X, Y ), ! apart_point_and_line( Y, line_connecting( X
% 1.48/1.87 , Y ) ) }.
% 1.48/1.87 { ! convergent_lines( X, Y ), ! apart_point_and_line( intersection_point( X
% 1.48/1.87 , Y ), X ) }.
% 1.48/1.87 { ! convergent_lines( X, Y ), ! apart_point_and_line( intersection_point( X
% 1.48/1.87 , Y ), Y ) }.
% 1.48/1.87 { ! distinct_points( X, Y ), ! distinct_lines( Z, T ), apart_point_and_line
% 1.48/1.87 ( X, Z ), apart_point_and_line( X, T ), apart_point_and_line( Y, Z ),
% 1.48/1.87 apart_point_and_line( Y, T ) }.
% 1.48/1.87 { ! apart_point_and_line( X, Y ), distinct_points( X, Z ),
% 1.48/1.87 apart_point_and_line( Z, Y ) }.
% 1.48/1.87 { ! apart_point_and_line( X, Y ), distinct_lines( Y, Z ),
% 1.48/1.87 apart_point_and_line( X, Z ) }.
% 1.48/1.87 { ! convergent_lines( X, Y ), distinct_lines( Y, Z ), convergent_lines( X,
% 1.48/1.87 Z ) }.
% 1.48/1.87 { ! convergent_lines( parallel_through_point( Y, X ), Y ) }.
% 1.48/1.87 { ! apart_point_and_line( X, parallel_through_point( Y, X ) ) }.
% 1.48/1.87 { ! distinct_lines( X, Y ), apart_point_and_line( Z, X ),
% 1.48/1.87 apart_point_and_line( Z, Y ), convergent_lines( X, Y ) }.
% 1.48/1.87 { convergent_lines( X, Y ), unorthogonal_lines( X, Y ) }.
% 1.48/1.87 { ! convergent_lines( X, Y ), ! unorthogonal_lines( X, Y ), alpha1( X, Z )
% 1.48/1.87 , convergent_lines( Y, Z ) }.
% 1.48/1.87 { ! convergent_lines( X, Y ), ! unorthogonal_lines( X, Y ), alpha1( X, Z )
% 1.48/1.87 , unorthogonal_lines( Y, Z ) }.
% 1.48/1.87 { ! alpha1( X, Y ), convergent_lines( X, Y ) }.
% 1.48/1.87 { ! alpha1( X, Y ), unorthogonal_lines( X, Y ) }.
% 1.48/1.87 { ! convergent_lines( X, Y ), ! unorthogonal_lines( X, Y ), alpha1( X, Y )
% 1.48/1.87 }.
% 1.48/1.87 { ! unorthogonal_lines( orthogonal_through_point( Y, X ), Y ) }.
% 1.48/1.87 { ! apart_point_and_line( X, orthogonal_through_point( Y, X ) ) }.
% 1.48/1.87 { ! distinct_lines( X, Y ), apart_point_and_line( Z, X ),
% 1.48/1.87 apart_point_and_line( Z, Y ), unorthogonal_lines( X, T ),
% 1.48/1.87 unorthogonal_lines( Y, T ) }.
% 1.48/1.87 { convergent_lines( skol1, skol2 ) }.
% 1.48/1.87 { ! unorthogonal_lines( skol1, skol3 ) }.
% 1.48/1.87 { ! unorthogonal_lines( skol2, skol3 ) }.
% 1.48/1.87
% 1.48/1.87 percentage equality = 0.000000, percentage horn = 0.586207
% 1.48/1.87 This a non-horn, non-equality problem
% 1.48/1.87
% 1.48/1.87
% 1.48/1.87 Options Used:
% 1.48/1.87
% 1.48/1.87 useres = 1
% 1.48/1.87 useparamod = 0
% 1.48/1.87 useeqrefl = 0
% 1.48/1.87 useeqfact = 0
% 1.48/1.87 usefactor = 1
% 1.48/1.87 usesimpsplitting = 0
% 1.48/1.87 usesimpdemod = 0
% 1.48/1.87 usesimpres = 3
% 1.48/1.87
% 1.48/1.87 resimpinuse = 1000
% 1.48/1.87 resimpclauses = 20000
% 1.48/1.87 substype = standard
% 1.48/1.87 backwardsubs = 1
% 1.48/1.87 selectoldest = 5
% 1.48/1.87
% 1.48/1.87 litorderings [0] = split
% 1.48/1.87 litorderings [1] = liftord
% 1.48/1.87
% 1.48/1.87 termordering = none
% 1.48/1.87
% 1.48/1.87 litapriori = 1
% 1.48/1.87 termapriori = 0
% 1.48/1.87 litaposteriori = 0
% 1.48/1.87 termaposteriori = 0
% 1.48/1.87 demodaposteriori = 0
% 1.48/1.87 ordereqreflfact = 0
% 1.48/1.87
% 1.48/1.87 litselect = none
% 1.48/1.87
% 1.48/1.87 maxweight = 15
% 1.48/1.87 maxdepth = 30000
% 1.48/1.87 maxlength = 115
% 1.48/1.87 maxnrvars = 195
% 1.48/1.87 excuselevel = 1
% 1.48/1.87 increasemaxweight = 1
% 1.48/1.87
% 1.48/1.87 maxselected = 10000000
% 1.48/1.87 maxnrclauses = 10000000
% 1.48/1.87
% 1.48/1.87 showgenerated = 0
% 1.48/1.87 showkept = 0
% 1.48/1.87 showselected = 0
% 1.48/1.87 showdeleted = 0
% 1.48/1.87 showresimp = 1
% 1.48/1.87 showstatus = 2000
% 1.48/1.87
% 1.48/1.87 prologoutput = 0
% 1.48/1.87 nrgoals = 5000000
% 1.48/1.87 totalproof = 1
% 1.48/1.87
% 1.48/1.87 Symbols occurring in the translation:
% 1.48/1.87
% 1.48/1.87 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 1.48/1.87 . [1, 2] (w:1, o:23, a:1, s:1, b:0),
% 1.48/1.87 ! [4, 1] (w:0, o:18, a:1, s:1, b:0),
% 1.48/1.87 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 1.48/1.87 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 1.48/1.87 distinct_points [36, 2] (w:1, o:48, a:1, s:1, b:0),
% 1.48/1.87 distinct_lines [37, 2] (w:1, o:49, a:1, s:1, b:0),
% 1.48/1.87 convergent_lines [38, 2] (w:1, o:47, a:1, s:1, b:0),
% 1.48/1.87 line_connecting [41, 2] (w:1, o:50, a:1, s:1, b:0),
% 1.48/1.87 apart_point_and_line [42, 2] (w:1, o:51, a:1, s:1, b:0),
% 1.48/1.87 intersection_point [43, 2] (w:1, o:52, a:1, s:1, b:0),
% 1.48/1.87 parallel_through_point [46, 2] (w:1, o:54, a:1, s:1, b:0),
% 1.48/1.87 unorthogonal_lines [49, 2] (w:1, o:55, a:1, s:1, b:0),
% 1.48/1.87 orthogonal_through_point [52, 2] (w:1, o:53, a:1, s:1, b:0),
% 1.48/1.87 alpha1 [53, 2] (w:1, o:56, a:1, s:1, b:0),
% 1.48/1.87 skol1 [54, 0] (w:1, o:15, a:1, s:1, b:0),
% 1.48/1.87 skol2 [55, 0] (w:1, o:16, a:1, s:1, b:0),
% 1.48/1.87 skol3 [56, 0] (w:1, o:17, a:1, s:1, b:0).
% 1.48/1.87
% 1.48/1.87
% 1.48/1.87 Starting Search:
% 1.48/1.87
% 1.48/1.87 *** allocated 15000 integers for clauses
% 1.48/1.87 *** allocated 22500 integers for clauses
% 1.48/1.87 *** allocated 33750 integers for clauses
% 1.48/1.87 *** allocated 15000 integers for termspace/termends
% 1.48/1.87 *** allocated 50625 integers for clauses
% 1.48/1.87 Resimplifying inuse:
% 1.48/1.87 Done
% 1.48/1.87
% 1.48/1.87 *** allocated 22500 integers for termspace/termends
% 1.48/1.87 *** allocated 75937 integers for clauses
% 1.48/1.87 *** allocated 33750 integers for termspace/termends
% 1.48/1.87 *** allocated 113905 integers for clauses
% 1.48/1.87
% 1.48/1.87 Intermediate Status:
% 1.48/1.87 Generated: 12337
% 1.48/1.87 Kept: 2009
% 1.48/1.87 Inuse: 290
% 1.48/1.87 Deleted: 0
% 1.48/1.87 Deletedinuse: 0
% 1.48/1.87
% 1.48/1.87 Resimplifying inuse:
% 1.48/1.87 Done
% 1.48/1.87
% 1.48/1.87 *** allocated 50625 integers for termspace/termends
% 1.48/1.87 *** allocated 170857 integers for clauses
% 1.48/1.87 Resimplifying inuse:
% 1.48/1.87 Done
% 1.48/1.87
% 1.48/1.87 *** allocated 75937 integers for termspace/termends
% 1.48/1.87
% 1.48/1.87 Intermediate Status:
% 1.48/1.87 Generated: 34071
% 1.48/1.87 Kept: 4046
% 1.48/1.87 Inuse: 489
% 1.48/1.87 Deleted: 0
% 1.48/1.87 Deletedinuse: 0
% 1.48/1.87
% 1.48/1.87 Resimplifying inuse:
% 1.48/1.87 Done
% 1.48/1.87
% 1.48/1.87 *** allocated 256285 integers for clauses
% 1.48/1.87 Resimplifying inuse:
% 1.48/1.87 Done
% 1.48/1.87
% 1.48/1.87 *** allocated 113905 integers for termspace/termends
% 1.48/1.87
% 1.48/1.87 Bliksems!, er is een bewijs:
% 1.48/1.87 % SZS status Theorem
% 1.48/1.87 % SZS output start Refutation
% 1.48/1.87
% 1.48/1.87 (1) {G0,W3,D2,L1,V1,M1} I { ! distinct_lines( X, X ) }.
% 1.48/1.87 (2) {G0,W3,D2,L1,V1,M1} I { ! convergent_lines( X, X ) }.
% 1.48/1.87 (4) {G0,W9,D2,L3,V3,M3} I { distinct_lines( X, Z ), distinct_lines( Y, Z )
% 1.48/1.87 , ! distinct_lines( X, Y ) }.
% 1.48/1.87 (5) {G0,W9,D2,L3,V3,M3} I { convergent_lines( X, Z ), convergent_lines( Y,
% 1.48/1.87 Z ), ! convergent_lines( X, Y ) }.
% 1.48/1.87 (8) {G0,W8,D3,L2,V2,M1} I { ! convergent_lines( X, Y ), !
% 1.48/1.87 apart_point_and_line( intersection_point( X, Y ), X ) }.
% 1.48/1.87 (9) {G0,W8,D3,L2,V2,M1} I { ! convergent_lines( X, Y ), !
% 1.48/1.87 apart_point_and_line( intersection_point( X, Y ), Y ) }.
% 1.48/1.87 (13) {G0,W9,D2,L3,V3,M1} I { ! convergent_lines( X, Y ), convergent_lines(
% 1.48/1.87 X, Z ), distinct_lines( Y, Z ) }.
% 1.48/1.87 (14) {G0,W5,D3,L1,V2,M1} I { ! convergent_lines( parallel_through_point( Y
% 1.48/1.87 , X ), Y ) }.
% 1.48/1.87 (17) {G0,W6,D2,L2,V2,M1} I { convergent_lines( X, Y ), unorthogonal_lines(
% 1.48/1.87 X, Y ) }.
% 1.48/1.87 (18) {G0,W12,D2,L4,V3,M1} I { ! convergent_lines( X, Y ), !
% 1.48/1.87 unorthogonal_lines( X, Y ), convergent_lines( Y, Z ), alpha1( X, Z ) }.
% 1.48/1.87 (21) {G0,W6,D2,L2,V2,M1} I { unorthogonal_lines( X, Y ), ! alpha1( X, Y )
% 1.48/1.87 }.
% 1.48/1.87 (25) {G0,W15,D2,L5,V4,M2} I { ! distinct_lines( X, Y ),
% 1.48/1.87 apart_point_and_line( Z, X ), apart_point_and_line( Z, Y ),
% 1.48/1.87 unorthogonal_lines( Y, T ), unorthogonal_lines( X, T ) }.
% 1.48/1.87 (26) {G0,W3,D2,L1,V0,M1} I { convergent_lines( skol1, skol2 ) }.
% 1.48/1.87 (27) {G0,W3,D2,L1,V0,M1} I { ! unorthogonal_lines( skol1, skol3 ) }.
% 1.48/1.87 (28) {G0,W3,D2,L1,V0,M1} I { ! unorthogonal_lines( skol2, skol3 ) }.
% 1.48/1.87 (34) {G1,W6,D2,L2,V2,M2} R(4,1) { ! distinct_lines( Y, X ), distinct_lines
% 1.48/1.87 ( X, Y ) }.
% 1.48/1.87 (43) {G1,W6,D2,L2,V1,M1} R(5,26) { convergent_lines( skol1, X ),
% 1.48/1.87 convergent_lines( skol2, X ) }.
% 1.48/1.87 (44) {G1,W6,D2,L2,V2,M2} R(5,2) { ! convergent_lines( Y, X ),
% 1.48/1.87 convergent_lines( X, Y ) }.
% 1.48/1.87 (47) {G2,W5,D3,L1,V2,M1} R(44,14) { ! convergent_lines( X,
% 1.48/1.87 parallel_through_point( X, Y ) ) }.
% 1.48/1.87 (49) {G3,W8,D3,L2,V3,M2} R(47,5) { ! convergent_lines( Y, X ),
% 1.48/1.87 convergent_lines( X, parallel_through_point( Y, Z ) ) }.
% 1.48/1.87 (53) {G1,W3,D2,L1,V0,M1} R(17,28) { convergent_lines( skol2, skol3 ) }.
% 1.48/1.87 (57) {G2,W6,D2,L2,V1,M1} R(53,5) { convergent_lines( skol2, X ),
% 1.48/1.87 convergent_lines( skol3, X ) }.
% 1.48/1.87 (61) {G3,W6,D2,L2,V1,M2} R(57,44) { convergent_lines( X, skol3 ),
% 1.48/1.87 convergent_lines( skol2, X ) }.
% 1.48/1.87 (124) {G2,W6,D2,L2,V1,M2} R(43,44) { convergent_lines( X, skol2 ),
% 1.48/1.87 convergent_lines( skol1, X ) }.
% 1.48/1.87 (141) {G3,W6,D2,L2,V1,M1} R(124,44) { convergent_lines( X, skol1 ),
% 1.48/1.87 convergent_lines( X, skol2 ) }.
% 1.48/1.87 (145) {G2,W9,D2,L3,V3,M1} R(13,34) { ! convergent_lines( X, Y ),
% 1.48/1.87 convergent_lines( X, Z ), distinct_lines( Z, Y ) }.
% 1.48/1.87 (183) {G1,W12,D2,L4,V3,M2} R(18,21) { ! convergent_lines( X, Y ),
% 1.48/1.87 convergent_lines( Y, Z ), unorthogonal_lines( X, Z ), !
% 1.48/1.87 unorthogonal_lines( X, Y ) }.
% 1.48/1.87 (240) {G4,W8,D3,L2,V3,M2} R(49,44) { convergent_lines(
% 1.48/1.87 parallel_through_point( X, Z ), Y ), ! convergent_lines( X, Y ) }.
% 1.48/1.87 (244) {G4,W7,D4,L1,V3,M1} R(49,14) { ! convergent_lines( X,
% 1.48/1.87 parallel_through_point( parallel_through_point( X, Y ), Z ) ) }.
% 1.48/1.87 (250) {G1,W12,D2,L4,V2,M1} R(25,27) { ! distinct_lines( X, skol1 ),
% 1.48/1.87 apart_point_and_line( Y, X ), apart_point_and_line( Y, skol1 ),
% 1.48/1.87 unorthogonal_lines( X, skol3 ) }.
% 1.48/1.87 (343) {G5,W8,D3,L2,V3,M2} R(240,44) { ! convergent_lines( Z, X ),
% 1.48/1.87 convergent_lines( parallel_through_point( X, Y ), Z ) }.
% 1.48/1.87 (346) {G6,W9,D5,L1,V4,M1} R(343,244) { ! convergent_lines(
% 1.48/1.87 parallel_through_point( parallel_through_point( parallel_through_point( X
% 1.48/1.87 , Y ), Z ), T ), X ) }.
% 1.48/1.87 (5015) {G4,W6,D2,L2,V1,M1} R(183,28);r(61) { convergent_lines( X, skol3 ),
% 1.48/1.87 ! unorthogonal_lines( skol2, X ) }.
% 1.48/1.87 (5121) {G5,W9,D2,L3,V1,M1} R(250,5015);r(2) { ! distinct_lines( skol2,
% 1.48/1.87 skol1 ), apart_point_and_line( X, skol1 ), apart_point_and_line( X, skol2
% 1.48/1.87 ) }.
% 1.48/1.87 (5327) {G6,W11,D3,L3,V1,M1} R(5121,9) { ! distinct_lines( skol2, skol1 ), !
% 1.48/1.87 convergent_lines( X, skol2 ), apart_point_and_line( intersection_point(
% 1.48/1.87 X, skol2 ), skol1 ) }.
% 1.48/1.87 (5526) {G7,W3,D2,L1,V0,M1} R(5327,8);f;r(26) { ! distinct_lines( skol2,
% 1.48/1.87 skol1 ) }.
% 1.48/1.87 (5605) {G8,W3,D2,L1,V1,M1} R(5526,145);r(141) { convergent_lines( X, skol2
% 1.48/1.87 ) }.
% 1.48/1.87 (5639) {G9,W0,D0,L0,V0,M0} R(5605,346) { }.
% 1.48/1.87
% 1.48/1.87
% 1.48/1.87 % SZS output end Refutation
% 1.48/1.87 found a proof!
% 1.48/1.87
% 1.48/1.87
% 1.48/1.87 Unprocessed initial clauses:
% 1.48/1.87
% 1.48/1.87 (5641) {G0,W3,D2,L1,V1,M1} { ! distinct_points( X, X ) }.
% 1.48/1.87 (5642) {G0,W3,D2,L1,V1,M1} { ! distinct_lines( X, X ) }.
% 1.48/1.87 (5643) {G0,W3,D2,L1,V1,M1} { ! convergent_lines( X, X ) }.
% 1.48/1.87 (5644) {G0,W9,D2,L3,V3,M3} { ! distinct_points( X, Y ), distinct_points( X
% 1.48/1.87 , Z ), distinct_points( Y, Z ) }.
% 1.48/1.87 (5645) {G0,W9,D2,L3,V3,M3} { ! distinct_lines( X, Y ), distinct_lines( X,
% 1.48/1.87 Z ), distinct_lines( Y, Z ) }.
% 1.48/1.87 (5646) {G0,W9,D2,L3,V3,M3} { ! convergent_lines( X, Y ), convergent_lines
% 1.48/1.87 ( X, Z ), convergent_lines( Y, Z ) }.
% 1.48/1.87 (5647) {G0,W8,D3,L2,V2,M2} { ! distinct_points( X, Y ), !
% 1.48/1.87 apart_point_and_line( X, line_connecting( X, Y ) ) }.
% 1.48/1.87 (5648) {G0,W8,D3,L2,V2,M2} { ! distinct_points( X, Y ), !
% 1.48/1.87 apart_point_and_line( Y, line_connecting( X, Y ) ) }.
% 1.48/1.87 (5649) {G0,W8,D3,L2,V2,M2} { ! convergent_lines( X, Y ), !
% 1.48/1.87 apart_point_and_line( intersection_point( X, Y ), X ) }.
% 1.48/1.87 (5650) {G0,W8,D3,L2,V2,M2} { ! convergent_lines( X, Y ), !
% 1.48/1.87 apart_point_and_line( intersection_point( X, Y ), Y ) }.
% 1.48/1.87 (5651) {G0,W18,D2,L6,V4,M6} { ! distinct_points( X, Y ), ! distinct_lines
% 1.48/1.87 ( Z, T ), apart_point_and_line( X, Z ), apart_point_and_line( X, T ),
% 1.48/1.87 apart_point_and_line( Y, Z ), apart_point_and_line( Y, T ) }.
% 1.48/1.87 (5652) {G0,W9,D2,L3,V3,M3} { ! apart_point_and_line( X, Y ),
% 1.48/1.87 distinct_points( X, Z ), apart_point_and_line( Z, Y ) }.
% 1.48/1.87 (5653) {G0,W9,D2,L3,V3,M3} { ! apart_point_and_line( X, Y ),
% 1.48/1.87 distinct_lines( Y, Z ), apart_point_and_line( X, Z ) }.
% 1.48/1.87 (5654) {G0,W9,D2,L3,V3,M3} { ! convergent_lines( X, Y ), distinct_lines( Y
% 1.48/1.87 , Z ), convergent_lines( X, Z ) }.
% 1.48/1.87 (5655) {G0,W5,D3,L1,V2,M1} { ! convergent_lines( parallel_through_point( Y
% 1.48/1.87 , X ), Y ) }.
% 1.48/1.87 (5656) {G0,W5,D3,L1,V2,M1} { ! apart_point_and_line( X,
% 1.48/1.87 parallel_through_point( Y, X ) ) }.
% 1.48/1.87 (5657) {G0,W12,D2,L4,V3,M4} { ! distinct_lines( X, Y ),
% 1.48/1.87 apart_point_and_line( Z, X ), apart_point_and_line( Z, Y ),
% 1.48/1.87 convergent_lines( X, Y ) }.
% 1.48/1.87 (5658) {G0,W6,D2,L2,V2,M2} { convergent_lines( X, Y ), unorthogonal_lines
% 1.48/1.87 ( X, Y ) }.
% 1.48/1.87 (5659) {G0,W12,D2,L4,V3,M4} { ! convergent_lines( X, Y ), !
% 1.48/1.87 unorthogonal_lines( X, Y ), alpha1( X, Z ), convergent_lines( Y, Z ) }.
% 1.48/1.87 (5660) {G0,W12,D2,L4,V3,M4} { ! convergent_lines( X, Y ), !
% 1.48/1.87 unorthogonal_lines( X, Y ), alpha1( X, Z ), unorthogonal_lines( Y, Z )
% 1.48/1.87 }.
% 1.48/1.87 (5661) {G0,W6,D2,L2,V2,M2} { ! alpha1( X, Y ), convergent_lines( X, Y )
% 1.48/1.87 }.
% 1.48/1.87 (5662) {G0,W6,D2,L2,V2,M2} { ! alpha1( X, Y ), unorthogonal_lines( X, Y )
% 1.48/1.87 }.
% 1.48/1.87 (5663) {G0,W9,D2,L3,V2,M3} { ! convergent_lines( X, Y ), !
% 1.48/1.87 unorthogonal_lines( X, Y ), alpha1( X, Y ) }.
% 1.48/1.87 (5664) {G0,W5,D3,L1,V2,M1} { ! unorthogonal_lines(
% 1.48/1.87 orthogonal_through_point( Y, X ), Y ) }.
% 1.48/1.87 (5665) {G0,W5,D3,L1,V2,M1} { ! apart_point_and_line( X,
% 1.48/1.87 orthogonal_through_point( Y, X ) ) }.
% 1.48/1.87 (5666) {G0,W15,D2,L5,V4,M5} { ! distinct_lines( X, Y ),
% 1.48/1.87 apart_point_and_line( Z, X ), apart_point_and_line( Z, Y ),
% 1.48/1.87 unorthogonal_lines( X, T ), unorthogonal_lines( Y, T ) }.
% 1.48/1.87 (5667) {G0,W3,D2,L1,V0,M1} { convergent_lines( skol1, skol2 ) }.
% 1.48/1.87 (5668) {G0,W3,D2,L1,V0,M1} { ! unorthogonal_lines( skol1, skol3 ) }.
% 1.48/1.87 (5669) {G0,W3,D2,L1,V0,M1} { ! unorthogonal_lines( skol2, skol3 ) }.
% 1.48/1.87
% 1.48/1.87
% 1.48/1.87 Total Proof:
% 1.48/1.87
% 1.48/1.87 subsumption: (1) {G0,W3,D2,L1,V1,M1} I { ! distinct_lines( X, X ) }.
% 1.48/1.87 parent0: (5642) {G0,W3,D2,L1,V1,M1} { ! distinct_lines( X, X ) }.
% 1.48/1.87 substitution0:
% 1.48/1.87 X := X
% 1.48/1.87 end
% 1.48/1.87 permutation0:
% 1.48/1.87 0 ==> 0
% 1.48/1.87 end
% 1.48/1.87
% 1.48/1.87 subsumption: (2) {G0,W3,D2,L1,V1,M1} I { ! convergent_lines( X, X ) }.
% 1.48/1.87 parent0: (5643) {G0,W3,D2,L1,V1,M1} { ! convergent_lines( X, X ) }.
% 1.48/1.87 substitution0:
% 1.48/1.87 X := X
% 1.48/1.87 end
% 1.48/1.87 permutation0:
% 1.48/1.87 0 ==> 0
% 1.48/1.87 end
% 1.48/1.87
% 1.48/1.87 subsumption: (4) {G0,W9,D2,L3,V3,M3} I { distinct_lines( X, Z ),
% 1.48/1.87 distinct_lines( Y, Z ), ! distinct_lines( X, Y ) }.
% 1.48/1.87 parent0: (5645) {G0,W9,D2,L3,V3,M3} { ! distinct_lines( X, Y ),
% 1.48/1.87 distinct_lines( X, Z ), distinct_lines( Y, Z ) }.
% 1.48/1.87 substitution0:
% 1.48/1.87 X := X
% 1.48/1.87 Y := Y
% 1.48/1.87 Z := Z
% 1.48/1.87 end
% 1.48/1.87 permutation0:
% 1.48/1.87 0 ==> 2
% 1.48/1.87 1 ==> 0
% 1.48/1.87 2 ==> 1
% 1.48/1.87 end
% 1.48/1.87
% 1.48/1.87 subsumption: (5) {G0,W9,D2,L3,V3,M3} I { convergent_lines( X, Z ),
% 1.48/1.87 convergent_lines( Y, Z ), ! convergent_lines( X, Y ) }.
% 1.48/1.87 parent0: (5646) {G0,W9,D2,L3,V3,M3} { ! convergent_lines( X, Y ),
% 1.48/1.87 convergent_lines( X, Z ), convergent_lines( Y, Z ) }.
% 1.48/1.87 substitution0:
% 1.48/1.87 X := X
% 1.48/1.87 Y := Y
% 1.48/1.87 Z := Z
% 1.48/1.87 end
% 1.48/1.87 permutation0:
% 1.48/1.87 0 ==> 2
% 1.48/1.87 1 ==> 0
% 1.48/1.87 2 ==> 1
% 1.48/1.87 end
% 1.48/1.87
% 1.48/1.87 subsumption: (8) {G0,W8,D3,L2,V2,M1} I { ! convergent_lines( X, Y ), !
% 1.48/1.87 apart_point_and_line( intersection_point( X, Y ), X ) }.
% 1.48/1.87 parent0: (5649) {G0,W8,D3,L2,V2,M2} { ! convergent_lines( X, Y ), !
% 1.48/1.87 apart_point_and_line( intersection_point( X, Y ), X ) }.
% 1.48/1.87 substitution0:
% 1.48/1.87 X := X
% 1.48/1.87 Y := Y
% 1.48/1.87 end
% 1.48/1.87 permutation0:
% 1.48/1.87 0 ==> 0
% 1.48/1.87 1 ==> 1
% 1.48/1.87 end
% 1.48/1.87
% 1.48/1.87 subsumption: (9) {G0,W8,D3,L2,V2,M1} I { ! convergent_lines( X, Y ), !
% 1.48/1.87 apart_point_and_line( intersection_point( X, Y ), Y ) }.
% 1.48/1.87 parent0: (5650) {G0,W8,D3,L2,V2,M2} { ! convergent_lines( X, Y ), !
% 1.48/1.87 apart_point_and_line( intersection_point( X, Y ), Y ) }.
% 1.48/1.87 substitution0:
% 1.48/1.87 X := X
% 1.48/1.87 Y := Y
% 1.48/1.87 end
% 1.48/1.87 permutation0:
% 1.48/1.87 0 ==> 0
% 1.48/1.87 1 ==> 1
% 1.48/1.87 end
% 1.48/1.87
% 1.48/1.87 subsumption: (13) {G0,W9,D2,L3,V3,M1} I { ! convergent_lines( X, Y ),
% 1.48/1.87 convergent_lines( X, Z ), distinct_lines( Y, Z ) }.
% 1.48/1.87 parent0: (5654) {G0,W9,D2,L3,V3,M3} { ! convergent_lines( X, Y ),
% 1.48/1.87 distinct_lines( Y, Z ), convergent_lines( X, Z ) }.
% 1.48/1.87 substitution0:
% 1.48/1.87 X := X
% 1.48/1.87 Y := Y
% 1.48/1.87 Z := Z
% 1.48/1.87 end
% 1.48/1.87 permutation0:
% 1.48/1.87 0 ==> 0
% 1.48/1.87 1 ==> 2
% 1.48/1.87 2 ==> 1
% 1.48/1.87 end
% 1.48/1.87
% 1.48/1.87 subsumption: (14) {G0,W5,D3,L1,V2,M1} I { ! convergent_lines(
% 1.48/1.87 parallel_through_point( Y, X ), Y ) }.
% 1.48/1.87 parent0: (5655) {G0,W5,D3,L1,V2,M1} { ! convergent_lines(
% 1.48/1.87 parallel_through_point( Y, X ), Y ) }.
% 1.48/1.87 substitution0:
% 1.48/1.87 X := X
% 1.48/1.87 Y := Y
% 1.48/1.87 end
% 1.48/1.87 permutation0:
% 1.48/1.87 0 ==> 0
% 1.48/1.87 end
% 1.48/1.87
% 1.48/1.87 subsumption: (17) {G0,W6,D2,L2,V2,M1} I { convergent_lines( X, Y ),
% 1.48/1.87 unorthogonal_lines( X, Y ) }.
% 1.48/1.87 parent0: (5658) {G0,W6,D2,L2,V2,M2} { convergent_lines( X, Y ),
% 1.48/1.87 unorthogonal_lines( X, Y ) }.
% 1.48/1.87 substitution0:
% 1.48/1.87 X := X
% 1.48/1.87 Y := Y
% 1.48/1.87 end
% 1.48/1.87 permutation0:
% 1.48/1.87 0 ==> 0
% 1.48/1.87 1 ==> 1
% 1.48/1.87 end
% 1.48/1.87
% 1.48/1.87 subsumption: (18) {G0,W12,D2,L4,V3,M1} I { ! convergent_lines( X, Y ), !
% 1.48/1.87 unorthogonal_lines( X, Y ), convergent_lines( Y, Z ), alpha1( X, Z ) }.
% 1.48/1.87 parent0: (5659) {G0,W12,D2,L4,V3,M4} { ! convergent_lines( X, Y ), !
% 1.48/1.87 unorthogonal_lines( X, Y ), alpha1( X, Z ), convergent_lines( Y, Z ) }.
% 1.48/1.87 substitution0:
% 1.48/1.87 X := X
% 1.48/1.87 Y := Y
% 1.48/1.87 Z := Z
% 1.48/1.87 end
% 1.48/1.87 permutation0:
% 1.48/1.87 0 ==> 0
% 1.48/1.87 1 ==> 1
% 1.48/1.87 2 ==> 3
% 1.48/1.87 3 ==> 2
% 1.48/1.87 end
% 1.48/1.87
% 1.48/1.87 subsumption: (21) {G0,W6,D2,L2,V2,M1} I { unorthogonal_lines( X, Y ), !
% 1.48/1.87 alpha1( X, Y ) }.
% 1.48/1.87 parent0: (5662) {G0,W6,D2,L2,V2,M2} { ! alpha1( X, Y ), unorthogonal_lines
% 1.48/1.87 ( X, Y ) }.
% 1.48/1.87 substitution0:
% 1.48/1.87 X := X
% 1.48/1.87 Y := Y
% 1.48/1.87 end
% 1.48/1.87 permutation0:
% 1.48/1.87 0 ==> 1
% 1.48/1.87 1 ==> 0
% 1.48/1.87 end
% 1.48/1.87
% 1.48/1.87 subsumption: (25) {G0,W15,D2,L5,V4,M2} I { ! distinct_lines( X, Y ),
% 1.48/1.87 apart_point_and_line( Z, X ), apart_point_and_line( Z, Y ),
% 1.48/1.87 unorthogonal_lines( Y, T ), unorthogonal_lines( X, T ) }.
% 1.48/1.87 parent0: (5666) {G0,W15,D2,L5,V4,M5} { ! distinct_lines( X, Y ),
% 1.48/1.87 apart_point_and_line( Z, X ), apart_point_and_line( Z, Y ),
% 1.48/1.87 unorthogonal_lines( X, T ), unorthogonal_lines( Y, T ) }.
% 1.48/1.87 substitution0:
% 1.48/1.87 X := X
% 1.48/1.87 Y := Y
% 1.48/1.87 Z := Z
% 1.48/1.87 T := T
% 1.48/1.87 end
% 1.48/1.87 permutation0:
% 1.48/1.87 0 ==> 0
% 1.48/1.87 1 ==> 1
% 1.48/1.87 2 ==> 2
% 1.48/1.87 3 ==> 4
% 1.48/1.87 4 ==> 3
% 1.48/1.87 end
% 1.48/1.87
% 1.48/1.87 subsumption: (26) {G0,W3,D2,L1,V0,M1} I { convergent_lines( skol1, skol2 )
% 1.48/1.87 }.
% 1.48/1.87 parent0: (5667) {G0,W3,D2,L1,V0,M1} { convergent_lines( skol1, skol2 ) }.
% 1.48/1.87 substitution0:
% 1.48/1.87 end
% 1.48/1.87 permutation0:
% 1.48/1.87 0 ==> 0
% 1.48/1.87 end
% 1.48/1.87
% 1.48/1.87 subsumption: (27) {G0,W3,D2,L1,V0,M1} I { ! unorthogonal_lines( skol1,
% 1.48/1.87 skol3 ) }.
% 1.48/1.87 parent0: (5668) {G0,W3,D2,L1,V0,M1} { ! unorthogonal_lines( skol1, skol3 )
% 1.48/1.87 }.
% 1.48/1.87 substitution0:
% 1.48/1.87 end
% 1.48/1.87 permutation0:
% 1.48/1.87 0 ==> 0
% 1.48/1.87 end
% 1.48/1.87
% 1.48/1.87 subsumption: (28) {G0,W3,D2,L1,V0,M1} I { ! unorthogonal_lines( skol2,
% 1.48/1.87 skol3 ) }.
% 1.48/1.87 parent0: (5669) {G0,W3,D2,L1,V0,M1} { ! unorthogonal_lines( skol2, skol3 )
% 1.48/1.87 }.
% 1.48/1.87 substitution0:
% 1.48/1.87 end
% 1.48/1.87 permutation0:
% 1.48/1.87 0 ==> 0
% 1.48/1.87 end
% 1.48/1.87
% 1.48/1.87 resolution: (5777) {G1,W6,D2,L2,V2,M2} { distinct_lines( Y, X ), !
% 1.48/1.87 distinct_lines( X, Y ) }.
% 1.48/1.87 parent0[0]: (1) {G0,W3,D2,L1,V1,M1} I { ! distinct_lines( X, X ) }.
% 1.48/1.87 parent1[0]: (4) {G0,W9,D2,L3,V3,M3} I { distinct_lines( X, Z ),
% 1.48/1.87 distinct_lines( Y, Z ), ! distinct_lines( X, Y ) }.
% 1.48/1.87 substitution0:
% 1.48/1.87 X := X
% 1.48/1.87 end
% 1.48/1.87 substitution1:
% 1.48/1.87 X := X
% 1.48/1.87 Y := Y
% 1.48/1.87 Z := X
% 1.48/1.87 end
% 1.48/1.87
% 1.48/1.87 subsumption: (34) {G1,W6,D2,L2,V2,M2} R(4,1) { ! distinct_lines( Y, X ),
% 1.48/1.87 distinct_lines( X, Y ) }.
% 1.48/1.87 parent0: (5777) {G1,W6,D2,L2,V2,M2} { distinct_lines( Y, X ), !
% 1.48/1.87 distinct_lines( X, Y ) }.
% 1.48/1.87 substitution0:
% 1.48/1.87 X := Y
% 1.48/1.87 Y := X
% 1.48/1.87 end
% 1.48/1.87 permutation0:
% 1.48/1.87 0 ==> 1
% 1.48/1.87 1 ==> 0
% 1.48/1.87 end
% 1.48/1.87
% 1.48/1.87 resolution: (5779) {G1,W6,D2,L2,V1,M2} { convergent_lines( skol1, X ),
% 1.48/1.87 convergent_lines( skol2, X ) }.
% 1.48/1.87 parent0[2]: (5) {G0,W9,D2,L3,V3,M3} I { convergent_lines( X, Z ),
% 1.48/1.87 convergent_lines( Y, Z ), ! convergent_lines( X, Y ) }.
% 1.48/1.87 parent1[0]: (26) {G0,W3,D2,L1,V0,M1} I { convergent_lines( skol1, skol2 )
% 1.48/1.87 }.
% 1.48/1.87 substitution0:
% 1.48/1.87 X := skol1
% 1.48/1.87 Y := skol2
% 1.48/1.87 Z := X
% 1.48/1.87 end
% 1.48/1.87 substitution1:
% 1.48/1.87 end
% 1.48/1.87
% 1.48/1.87 subsumption: (43) {G1,W6,D2,L2,V1,M1} R(5,26) { convergent_lines( skol1, X
% 1.48/1.87 ), convergent_lines( skol2, X ) }.
% 1.48/1.87 parent0: (5779) {G1,W6,D2,L2,V1,M2} { convergent_lines( skol1, X ),
% 1.48/1.87 convergent_lines( skol2, X ) }.
% 1.48/1.87 substitution0:
% 1.48/1.87 X := X
% 1.48/1.87 end
% 1.48/1.87 permutation0:
% 1.48/1.87 0 ==> 0
% 1.48/1.87 1 ==> 1
% 1.48/1.87 end
% 1.48/1.87
% 1.48/1.87 resolution: (5780) {G1,W6,D2,L2,V2,M2} { convergent_lines( Y, X ), !
% 1.48/1.87 convergent_lines( X, Y ) }.
% 1.48/1.87 parent0[0]: (2) {G0,W3,D2,L1,V1,M1} I { ! convergent_lines( X, X ) }.
% 1.48/1.87 parent1[0]: (5) {G0,W9,D2,L3,V3,M3} I { convergent_lines( X, Z ),
% 1.48/1.87 convergent_lines( Y, Z ), ! convergent_lines( X, Y ) }.
% 1.48/1.87 substitution0:
% 1.48/1.87 X := X
% 1.48/1.87 end
% 1.48/1.87 substitution1:
% 1.48/1.87 X := X
% 1.48/1.87 Y := Y
% 1.48/1.87 Z := X
% 1.48/1.87 end
% 1.48/1.87
% 1.48/1.87 subsumption: (44) {G1,W6,D2,L2,V2,M2} R(5,2) { ! convergent_lines( Y, X ),
% 1.48/1.87 convergent_lines( X, Y ) }.
% 1.48/1.87 parent0: (5780) {G1,W6,D2,L2,V2,M2} { convergent_lines( Y, X ), !
% 1.48/1.87 convergent_lines( X, Y ) }.
% 1.48/1.87 substitution0:
% 1.48/1.87 X := Y
% 1.48/1.87 Y := X
% 1.48/1.87 end
% 1.48/1.87 permutation0:
% 1.48/1.87 0 ==> 1
% 1.48/1.87 1 ==> 0
% 1.48/1.87 end
% 1.48/1.87
% 1.48/1.87 resolution: (5782) {G1,W5,D3,L1,V2,M1} { ! convergent_lines( X,
% 1.48/1.87 parallel_through_point( X, Y ) ) }.
% 1.48/1.87 parent0[0]: (14) {G0,W5,D3,L1,V2,M1} I { ! convergent_lines(
% 1.48/1.87 parallel_through_point( Y, X ), Y ) }.
% 1.48/1.87 parent1[1]: (44) {G1,W6,D2,L2,V2,M2} R(5,2) { ! convergent_lines( Y, X ),
% 1.48/1.87 convergent_lines( X, Y ) }.
% 1.48/1.87 substitution0:
% 1.48/1.87 X := Y
% 1.48/1.87 Y := X
% 1.48/1.87 end
% 1.48/1.87 substitution1:
% 1.48/1.87 X := parallel_through_point( X, Y )
% 1.48/1.87 Y := X
% 1.48/1.87 end
% 1.48/1.87
% 1.48/1.87 subsumption: (47) {G2,W5,D3,L1,V2,M1} R(44,14) { ! convergent_lines( X,
% 1.48/1.87 parallel_through_point( X, Y ) ) }.
% 1.48/1.87 parent0: (5782) {G1,W5,D3,L1,V2,M1} { ! convergent_lines( X,
% 1.48/1.87 parallel_through_point( X, Y ) ) }.
% 1.48/1.87 substitution0:
% 1.48/1.87 X := X
% 1.48/1.87 Y := Y
% 1.48/1.87 end
% 1.48/1.87 permutation0:
% 1.48/1.87 0 ==> 0
% 1.48/1.87 end
% 1.48/1.87
% 1.48/1.87 resolution: (5783) {G1,W8,D3,L2,V3,M2} { convergent_lines( Z,
% 1.48/1.87 parallel_through_point( X, Y ) ), ! convergent_lines( X, Z ) }.
% 1.48/1.87 parent0[0]: (47) {G2,W5,D3,L1,V2,M1} R(44,14) { ! convergent_lines( X,
% 1.48/1.87 parallel_through_point( X, Y ) ) }.
% 1.48/1.87 parent1[0]: (5) {G0,W9,D2,L3,V3,M3} I { convergent_lines( X, Z ),
% 1.48/1.87 convergent_lines( Y, Z ), ! convergent_lines( X, Y ) }.
% 1.48/1.87 substitution0:
% 1.48/1.87 X := X
% 1.48/1.87 Y := Y
% 1.48/1.87 end
% 1.48/1.87 substitution1:
% 1.48/1.87 X := X
% 1.48/1.87 Y := Z
% 1.48/1.87 Z := parallel_through_point( X, Y )
% 1.48/1.87 end
% 1.48/1.87
% 1.48/1.87 subsumption: (49) {G3,W8,D3,L2,V3,M2} R(47,5) { ! convergent_lines( Y, X )
% 1.48/1.87 , convergent_lines( X, parallel_through_point( Y, Z ) ) }.
% 1.48/1.87 parent0: (5783) {G1,W8,D3,L2,V3,M2} { convergent_lines( Z,
% 1.48/1.87 parallel_through_point( X, Y ) ), ! convergent_lines( X, Z ) }.
% 1.48/1.87 substitution0:
% 1.48/1.87 X := Y
% 1.48/1.87 Y := Z
% 1.48/1.87 Z := X
% 1.48/1.87 end
% 1.48/1.87 permutation0:
% 1.48/1.87 0 ==> 1
% 1.48/1.87 1 ==> 0
% 1.48/1.87 end
% 1.48/1.87
% 1.48/1.87 resolution: (5785) {G1,W3,D2,L1,V0,M1} { convergent_lines( skol2, skol3 )
% 1.48/1.87 }.
% 1.48/1.87 parent0[0]: (28) {G0,W3,D2,L1,V0,M1} I { ! unorthogonal_lines( skol2, skol3
% 1.48/1.87 ) }.
% 1.48/1.87 parent1[1]: (17) {G0,W6,D2,L2,V2,M1} I { convergent_lines( X, Y ),
% 1.48/1.87 unorthogonal_lines( X, Y ) }.
% 1.48/1.87 substitution0:
% 1.48/1.87 end
% 1.48/1.87 substitution1:
% 1.48/1.87 X := skol2
% 1.48/1.87 Y := skol3
% 1.48/1.87 end
% 1.48/1.87
% 1.48/1.87 subsumption: (53) {G1,W3,D2,L1,V0,M1} R(17,28) { convergent_lines( skol2,
% 1.48/1.87 skol3 ) }.
% 1.48/1.87 parent0: (5785) {G1,W3,D2,L1,V0,M1} { convergent_lines( skol2, skol3 ) }.
% 1.48/1.87 substitution0:
% 1.48/1.87 end
% 1.48/1.87 permutation0:
% 1.48/1.87 0 ==> 0
% 1.48/1.87 end
% 1.48/1.87
% 1.48/1.87 resolution: (5786) {G1,W6,D2,L2,V1,M2} { convergent_lines( skol2, X ),
% 1.48/1.87 convergent_lines( skol3, X ) }.
% 1.48/1.87 parent0[2]: (5) {G0,W9,D2,L3,V3,M3} I { convergent_lines( X, Z ),
% 1.48/1.87 convergent_lines( Y, Z ), ! convergent_lines( X, Y ) }.
% 1.48/1.87 parent1[0]: (53) {G1,W3,D2,L1,V0,M1} R(17,28) { convergent_lines( skol2,
% 1.48/1.87 skol3 ) }.
% 1.48/1.87 substitution0:
% 1.48/1.87 X := skol2
% 1.48/1.87 Y := skol3
% 1.48/1.87 Z := X
% 1.48/1.87 end
% 1.48/1.87 substitution1:
% 1.48/1.87 end
% 1.48/1.87
% 1.48/1.87 subsumption: (57) {G2,W6,D2,L2,V1,M1} R(53,5) { convergent_lines( skol2, X
% 1.48/1.87 ), convergent_lines( skol3, X ) }.
% 1.48/1.87 parent0: (5786) {G1,W6,D2,L2,V1,M2} { convergent_lines( skol2, X ),
% 1.48/1.87 convergent_lines( skol3, X ) }.
% 1.48/1.87 substitution0:
% 1.48/1.87 X := X
% 1.48/1.87 end
% 1.48/1.87 permutation0:
% 1.48/1.87 0 ==> 0
% 1.48/1.87 1 ==> 1
% 1.48/1.87 end
% 1.48/1.87
% 1.48/1.87 resolution: (5788) {G2,W6,D2,L2,V1,M2} { convergent_lines( X, skol3 ),
% 1.48/1.87 convergent_lines( skol2, X ) }.
% 1.48/1.87 parent0[0]: (44) {G1,W6,D2,L2,V2,M2} R(5,2) { ! convergent_lines( Y, X ),
% 1.48/1.87 convergent_lines( X, Y ) }.
% 1.48/1.87 parent1[1]: (57) {G2,W6,D2,L2,V1,M1} R(53,5) { convergent_lines( skol2, X )
% 1.48/1.87 , convergent_lines( skol3, X ) }.
% 1.48/1.87 substitution0:
% 1.48/1.87 X := X
% 1.48/1.87 Y := skol3
% 1.48/1.87 end
% 1.48/1.87 substitution1:
% 1.48/1.87 X := X
% 1.48/1.87 end
% 1.48/1.87
% 1.48/1.87 subsumption: (61) {G3,W6,D2,L2,V1,M2} R(57,44) { convergent_lines( X, skol3
% 1.48/1.87 ), convergent_lines( skol2, X ) }.
% 1.48/1.87 parent0: (5788) {G2,W6,D2,L2,V1,M2} { convergent_lines( X, skol3 ),
% 1.48/1.87 convergent_lines( skol2, X ) }.
% 1.48/1.87 substitution0:
% 1.48/1.87 X := X
% 1.48/1.87 end
% 1.48/1.87 permutation0:
% 1.48/1.87 0 ==> 0
% 1.48/1.87 1 ==> 1
% 1.48/1.87 end
% 1.48/1.87
% 1.48/1.87 resolution: (5790) {G2,W6,D2,L2,V1,M2} { convergent_lines( X, skol2 ),
% 1.48/1.87 convergent_lines( skol1, X ) }.
% 1.48/1.87 parent0[0]: (44) {G1,W6,D2,L2,V2,M2} R(5,2) { ! convergent_lines( Y, X ),
% 1.48/1.87 convergent_lines( X, Y ) }.
% 1.48/1.87 parent1[1]: (43) {G1,W6,D2,L2,V1,M1} R(5,26) { convergent_lines( skol1, X )
% 1.48/1.87 , convergent_lines( skol2, X ) }.
% 1.48/1.87 substitution0:
% 1.48/1.87 X := X
% 1.48/1.87 Y := skol2
% 1.48/1.87 end
% 1.48/1.87 substitution1:
% 1.48/1.87 X := X
% 1.48/1.87 end
% 1.48/1.87
% 1.48/1.87 subsumption: (124) {G2,W6,D2,L2,V1,M2} R(43,44) { convergent_lines( X,
% 1.48/1.87 skol2 ), convergent_lines( skol1, X ) }.
% 1.48/1.87 parent0: (5790) {G2,W6,D2,L2,V1,M2} { convergent_lines( X, skol2 ),
% 1.48/1.87 convergent_lines( skol1, X ) }.
% 1.48/1.87 substitution0:
% 1.48/1.87 X := X
% 1.48/1.87 end
% 1.48/1.87 permutation0:
% 1.48/1.87 0 ==> 0
% 1.48/1.87 1 ==> 1
% 1.48/1.87 end
% 1.48/1.87
% 1.48/1.87 resolution: (5792) {G2,W6,D2,L2,V1,M2} { convergent_lines( X, skol1 ),
% 1.48/1.87 convergent_lines( X, skol2 ) }.
% 1.48/1.87 parent0[0]: (44) {G1,W6,D2,L2,V2,M2} R(5,2) { ! convergent_lines( Y, X ),
% 1.48/1.87 convergent_lines( X, Y ) }.
% 1.48/1.87 parent1[1]: (124) {G2,W6,D2,L2,V1,M2} R(43,44) { convergent_lines( X, skol2
% 1.48/1.87 ), convergent_lines( skol1, X ) }.
% 1.48/1.87 substitution0:
% 1.48/1.87 X := X
% 1.48/1.87 Y := skol1
% 1.48/1.87 end
% 1.48/1.87 substitution1:
% 1.48/1.87 X := X
% 1.48/1.87 end
% 1.48/1.87
% 1.48/1.87 subsumption: (141) {G3,W6,D2,L2,V1,M1} R(124,44) { convergent_lines( X,
% 1.48/1.87 skol1 ), convergent_lines( X, skol2 ) }.
% 1.48/1.87 parent0: (5792) {G2,W6,D2,L2,V1,M2} { convergent_lines( X, skol1 ),
% 1.48/1.87 convergent_lines( X, skol2 ) }.
% 1.48/1.87 substitution0:
% 1.48/1.87 X := X
% 1.48/1.87 end
% 1.48/1.87 permutation0:
% 1.48/1.87 0 ==> 0
% 1.48/1.87 1 ==> 1
% 1.48/1.87 end
% 1.48/1.87
% 1.48/1.87 resolution: (5793) {G1,W9,D2,L3,V3,M3} { distinct_lines( Y, X ), !
% 1.48/1.87 convergent_lines( Z, X ), convergent_lines( Z, Y ) }.
% 1.48/1.87 parent0[0]: (34) {G1,W6,D2,L2,V2,M2} R(4,1) { ! distinct_lines( Y, X ),
% 1.48/1.87 distinct_lines( X, Y ) }.
% 1.48/1.87 parent1[2]: (13) {G0,W9,D2,L3,V3,M1} I { ! convergent_lines( X, Y ),
% 1.48/1.87 convergent_lines( X, Z ), distinct_lines( Y, Z ) }.
% 1.48/1.87 substitution0:
% 1.48/1.87 X := Y
% 1.48/1.87 Y := X
% 1.48/1.87 end
% 1.48/1.87 substitution1:
% 1.48/1.87 X := Z
% 1.48/1.87 Y := X
% 1.48/1.87 Z := Y
% 1.48/1.87 end
% 1.48/1.87
% 1.48/1.87 subsumption: (145) {G2,W9,D2,L3,V3,M1} R(13,34) { ! convergent_lines( X, Y
% 1.48/1.87 ), convergent_lines( X, Z ), distinct_lines( Z, Y ) }.
% 1.48/1.87 parent0: (5793) {G1,W9,D2,L3,V3,M3} { distinct_lines( Y, X ), !
% 1.48/1.87 convergent_lines( Z, X ), convergent_lines( Z, Y ) }.
% 1.48/1.87 substitution0:
% 1.48/1.87 X := Y
% 1.48/1.87 Y := Z
% 1.48/1.87 Z := X
% 1.48/1.87 end
% 1.48/1.87 permutation0:
% 1.48/1.87 0 ==> 2
% 1.48/1.87 1 ==> 0
% 1.48/1.87 2 ==> 1
% 1.48/1.87 end
% 1.48/1.87
% 1.48/1.87 resolution: (5795) {G1,W12,D2,L4,V3,M4} { unorthogonal_lines( X, Y ), !
% 1.48/1.87 convergent_lines( X, Z ), ! unorthogonal_lines( X, Z ), convergent_lines
% 1.48/1.87 ( Z, Y ) }.
% 1.48/1.87 parent0[1]: (21) {G0,W6,D2,L2,V2,M1} I { unorthogonal_lines( X, Y ), !
% 1.48/1.87 alpha1( X, Y ) }.
% 1.48/1.87 parent1[3]: (18) {G0,W12,D2,L4,V3,M1} I { ! convergent_lines( X, Y ), !
% 1.48/1.87 unorthogonal_lines( X, Y ), convergent_lines( Y, Z ), alpha1( X, Z ) }.
% 1.48/1.87 substitution0:
% 1.48/1.87 X := X
% 1.48/1.87 Y := Y
% 1.48/1.87 end
% 1.48/1.87 substitution1:
% 1.48/1.87 X := X
% 1.48/1.87 Y := Z
% 1.48/1.87 Z := Y
% 1.48/1.87 end
% 1.48/1.87
% 1.48/1.87 subsumption: (183) {G1,W12,D2,L4,V3,M2} R(18,21) { ! convergent_lines( X, Y
% 1.48/1.87 ), convergent_lines( Y, Z ), unorthogonal_lines( X, Z ), !
% 1.48/1.87 unorthogonal_lines( X, Y ) }.
% 1.48/1.87 parent0: (5795) {G1,W12,D2,L4,V3,M4} { unorthogonal_lines( X, Y ), !
% 1.48/1.87 convergent_lines( X, Z ), ! unorthogonal_lines( X, Z ), convergent_lines
% 1.48/1.87 ( Z, Y ) }.
% 1.48/1.87 substitution0:
% 1.48/1.87 X := X
% 1.48/1.87 Y := Z
% 1.48/1.87 Z := Y
% 1.48/1.87 end
% 1.48/1.87 permutation0:
% 1.48/1.87 0 ==> 2
% 1.48/1.87 1 ==> 0
% 1.48/1.87 2 ==> 3
% 1.48/1.87 3 ==> 1
% 1.48/1.87 end
% 1.48/1.87
% 1.48/1.87 resolution: (5797) {G2,W8,D3,L2,V3,M2} { convergent_lines(
% 1.48/1.87 parallel_through_point( Y, Z ), X ), ! convergent_lines( Y, X ) }.
% 1.48/1.87 parent0[0]: (44) {G1,W6,D2,L2,V2,M2} R(5,2) { ! convergent_lines( Y, X ),
% 1.48/1.87 convergent_lines( X, Y ) }.
% 1.48/1.87 parent1[1]: (49) {G3,W8,D3,L2,V3,M2} R(47,5) { ! convergent_lines( Y, X ),
% 1.48/1.87 convergent_lines( X, parallel_through_point( Y, Z ) ) }.
% 1.48/1.87 substitution0:
% 1.48/1.87 X := parallel_through_point( Y, Z )
% 1.48/1.87 Y := X
% 1.48/1.87 end
% 1.48/1.87 substitution1:
% 1.48/1.87 X := X
% 1.48/1.87 Y := Y
% 1.48/1.87 Z := Z
% 1.48/1.87 end
% 1.48/1.87
% 1.48/1.87 subsumption: (240) {G4,W8,D3,L2,V3,M2} R(49,44) { convergent_lines(
% 1.48/1.87 parallel_through_point( X, Z ), Y ), ! convergent_lines( X, Y ) }.
% 1.48/1.87 parent0: (5797) {G2,W8,D3,L2,V3,M2} { convergent_lines(
% 1.48/1.87 parallel_through_point( Y, Z ), X ), ! convergent_lines( Y, X ) }.
% 1.48/1.87 substitution0:
% 1.48/1.87 X := Y
% 1.48/1.87 Y := X
% 1.48/1.87 Z := Z
% 1.48/1.87 end
% 1.48/1.87 permutation0:
% 1.48/1.87 0 ==> 0
% 1.48/1.87 1 ==> 1
% 1.48/1.87 end
% 1.48/1.87
% 1.48/1.87 resolution: (5798) {G1,W7,D4,L1,V3,M1} { ! convergent_lines( X,
% 1.48/1.87 parallel_through_point( parallel_through_point( X, Y ), Z ) ) }.
% 1.48/1.87 parent0[0]: (14) {G0,W5,D3,L1,V2,M1} I { ! convergent_lines(
% 1.48/1.87 parallel_through_point( Y, X ), Y ) }.
% 1.48/1.87 parent1[1]: (49) {G3,W8,D3,L2,V3,M2} R(47,5) { ! convergent_lines( Y, X ),
% 1.48/1.87 convergent_lines( X, parallel_through_point( Y, Z ) ) }.
% 1.48/1.87 substitution0:
% 1.48/1.87 X := Z
% 1.48/1.87 Y := parallel_through_point( X, Y )
% 1.48/1.87 end
% 1.48/1.87 substitution1:
% 1.48/1.87 X := parallel_through_point( parallel_through_point( X, Y ), Z )
% 1.48/1.87 Y := X
% 1.48/1.87 Z := Y
% 1.48/1.87 end
% 1.48/1.87
% 1.48/1.87 subsumption: (244) {G4,W7,D4,L1,V3,M1} R(49,14) { ! convergent_lines( X,
% 1.48/1.87 parallel_through_point( parallel_through_point( X, Y ), Z ) ) }.
% 1.48/1.87 parent0: (5798) {G1,W7,D4,L1,V3,M1} { ! convergent_lines( X,
% 1.48/1.87 parallel_through_point( parallel_through_point( X, Y ), Z ) ) }.
% 1.48/1.87 substitution0:
% 1.48/1.87 X := X
% 1.48/1.87 Y := Y
% 1.48/1.87 Z := Z
% 1.48/1.87 end
% 1.48/1.87 permutation0:
% 1.48/1.87 0 ==> 0
% 1.48/1.87 end
% 1.48/1.87
% 1.48/1.87 resolution: (5799) {G1,W12,D2,L4,V2,M4} { ! distinct_lines( X, skol1 ),
% 1.48/1.87 apart_point_and_line( Y, X ), apart_point_and_line( Y, skol1 ),
% 1.48/1.87 unorthogonal_lines( X, skol3 ) }.
% 1.48/1.87 parent0[0]: (27) {G0,W3,D2,L1,V0,M1} I { ! unorthogonal_lines( skol1, skol3
% 1.48/1.87 ) }.
% 1.48/1.87 parent1[3]: (25) {G0,W15,D2,L5,V4,M2} I { ! distinct_lines( X, Y ),
% 1.48/1.87 apart_point_and_line( Z, X ), apart_point_and_line( Z, Y ),
% 1.48/1.87 unorthogonal_lines( Y, T ), unorthogonal_lines( X, T ) }.
% 1.48/1.87 substitution0:
% 1.48/1.87 end
% 1.48/1.87 substitution1:
% 1.48/1.87 X := X
% 1.48/1.87 Y := skol1
% 1.48/1.87 Z := Y
% 1.48/1.87 T := skol3
% 1.48/1.87 end
% 1.48/1.87
% 1.48/1.87 subsumption: (250) {G1,W12,D2,L4,V2,M1} R(25,27) { ! distinct_lines( X,
% 1.48/1.87 skol1 ), apart_point_and_line( Y, X ), apart_point_and_line( Y, skol1 ),
% 1.48/1.87 unorthogonal_lines( X, skol3 ) }.
% 1.48/1.87 parent0: (5799) {G1,W12,D2,L4,V2,M4} { ! distinct_lines( X, skol1 ),
% 1.48/1.87 apart_point_and_line( Y, X ), apart_point_and_line( Y, skol1 ),
% 1.48/1.87 unorthogonal_lines( X, skol3 ) }.
% 1.48/1.87 substitution0:
% 1.48/1.87 X := X
% 1.48/1.87 Y := Y
% 1.48/1.87 end
% 1.48/1.87 permutation0:
% 1.48/1.87 0 ==> 0
% 1.48/1.87 1 ==> 1
% 1.48/1.87 2 ==> 2
% 1.48/1.87 3 ==> 3
% 1.48/1.87 end
% 1.48/1.87
% 1.48/1.87 resolution: (5802) {G2,W8,D3,L2,V3,M2} { convergent_lines(
% 1.48/1.87 parallel_through_point( X, Y ), Z ), ! convergent_lines( Z, X ) }.
% 1.48/1.87 parent0[1]: (240) {G4,W8,D3,L2,V3,M2} R(49,44) { convergent_lines(
% 1.48/1.87 parallel_through_point( X, Z ), Y ), ! convergent_lines( X, Y ) }.
% 1.48/1.87 parent1[1]: (44) {G1,W6,D2,L2,V2,M2} R(5,2) { ! convergent_lines( Y, X ),
% 1.48/1.87 convergent_lines( X, Y ) }.
% 1.48/1.87 substitution0:
% 1.48/1.87 X := X
% 1.48/1.87 Y := Z
% 1.48/1.87 Z := Y
% 1.48/1.87 end
% 1.48/1.87 substitution1:
% 1.48/1.87 X := X
% 1.48/1.87 Y := Z
% 1.48/1.87 end
% 1.48/1.87
% 1.48/1.87 subsumption: (343) {G5,W8,D3,L2,V3,M2} R(240,44) { ! convergent_lines( Z, X
% 1.48/1.87 ), convergent_lines( parallel_through_point( X, Y ), Z ) }.
% 1.48/1.87 parent0: (5802) {G2,W8,D3,L2,V3,M2} { convergent_lines(
% 1.48/1.87 parallel_through_point( X, Y ), Z ), ! convergent_lines( Z, X ) }.
% 1.48/1.87 substitution0:
% 1.48/1.87 X := X
% 1.48/1.87 Y := Y
% 1.48/1.87 Z := Z
% 1.48/1.87 end
% 1.48/1.87 permutation0:
% 1.48/1.87 0 ==> 1
% 1.48/1.87 1 ==> 0
% 1.48/1.87 end
% 1.48/1.87
% 1.48/1.87 resolution: (5803) {G5,W9,D5,L1,V4,M1} { ! convergent_lines(
% 1.48/1.87 parallel_through_point( parallel_through_point( parallel_through_point( X
% 1.48/1.87 , Y ), Z ), T ), X ) }.
% 1.48/1.87 parent0[0]: (244) {G4,W7,D4,L1,V3,M1} R(49,14) { ! convergent_lines( X,
% 1.48/1.87 parallel_through_point( parallel_through_point( X, Y ), Z ) ) }.
% 1.48/1.87 parent1[1]: (343) {G5,W8,D3,L2,V3,M2} R(240,44) { ! convergent_lines( Z, X
% 1.48/1.87 ), convergent_lines( parallel_through_point( X, Y ), Z ) }.
% 1.48/1.87 substitution0:
% 1.48/1.87 X := parallel_through_point( X, Y )
% 1.48/1.87 Y := Z
% 1.48/1.87 Z := T
% 1.48/1.87 end
% 1.48/1.87 substitution1:
% 1.48/1.87 X := X
% 1.48/1.87 Y := Y
% 1.48/1.87 Z := parallel_through_point( parallel_through_point(
% 1.48/1.87 parallel_through_point( X, Y ), Z ), T )
% 1.48/1.87 end
% 1.48/1.87
% 1.48/1.87 subsumption: (346) {G6,W9,D5,L1,V4,M1} R(343,244) { ! convergent_lines(
% 1.48/1.87 parallel_through_point( parallel_through_point( parallel_through_point( X
% 1.48/1.87 , Y ), Z ), T ), X ) }.
% 1.48/1.87 parent0: (5803) {G5,W9,D5,L1,V4,M1} { ! convergent_lines(
% 1.48/1.87 parallel_through_point( parallel_through_point( parallel_through_point( X
% 1.48/1.87 , Y ), Z ), T ), X ) }.
% 1.48/1.87 substitution0:
% 1.48/1.87 X := X
% 1.48/1.87 Y := Y
% 1.48/1.87 Z := Z
% 1.48/1.87 T := T
% 1.48/1.87 end
% 1.48/1.87 permutation0:
% 1.48/1.87 0 ==> 0
% 1.48/1.87 end
% 1.48/1.87
% 1.48/1.87 resolution: (5804) {G1,W9,D2,L3,V1,M3} { ! convergent_lines( skol2, X ),
% 1.48/1.87 convergent_lines( X, skol3 ), ! unorthogonal_lines( skol2, X ) }.
% 1.48/1.87 parent0[0]: (28) {G0,W3,D2,L1,V0,M1} I { ! unorthogonal_lines( skol2, skol3
% 1.48/1.87 ) }.
% 1.48/1.87 parent1[2]: (183) {G1,W12,D2,L4,V3,M2} R(18,21) { ! convergent_lines( X, Y
% 1.48/1.87 ), convergent_lines( Y, Z ), unorthogonal_lines( X, Z ), !
% 1.48/1.87 unorthogonal_lines( X, Y ) }.
% 1.48/1.87 substitution0:
% 1.48/1.87 end
% 1.48/1.87 substitution1:
% 1.48/1.87 X := skol2
% 1.48/1.87 Y := X
% 1.48/1.87 Z := skol3
% 1.48/1.87 end
% 1.48/1.87
% 1.48/1.87 resolution: (5805) {G2,W9,D2,L3,V1,M3} { convergent_lines( X, skol3 ), !
% 1.48/1.87 unorthogonal_lines( skol2, X ), convergent_lines( X, skol3 ) }.
% 1.48/1.87 parent0[0]: (5804) {G1,W9,D2,L3,V1,M3} { ! convergent_lines( skol2, X ),
% 1.48/1.87 convergent_lines( X, skol3 ), ! unorthogonal_lines( skol2, X ) }.
% 1.48/1.87 parent1[1]: (61) {G3,W6,D2,L2,V1,M2} R(57,44) { convergent_lines( X, skol3
% 1.48/1.87 ), convergent_lines( skol2, X ) }.
% 1.48/1.87 substitution0:
% 1.48/1.87 X := X
% 1.48/1.87 end
% 1.48/1.87 substitution1:
% 1.48/1.87 X := X
% 1.48/1.87 end
% 1.48/1.87
% 1.48/1.87 factor: (5806) {G2,W6,D2,L2,V1,M2} { convergent_lines( X, skol3 ), !
% 1.48/1.87 unorthogonal_lines( skol2, X ) }.
% 1.48/1.87 parent0[0, 2]: (5805) {G2,W9,D2,L3,V1,M3} { convergent_lines( X, skol3 ),
% 1.48/1.87 ! unorthogonal_lines( skol2, X ), convergent_lines( X, skol3 ) }.
% 1.48/1.87 substitution0:
% 1.48/1.87 X := X
% 1.48/1.87 end
% 1.48/1.87
% 1.48/1.87 subsumption: (5015) {G4,W6,D2,L2,V1,M1} R(183,28);r(61) { convergent_lines
% 1.48/1.87 ( X, skol3 ), ! unorthogonal_lines( skol2, X ) }.
% 1.48/1.87 parent0: (5806) {G2,W6,D2,L2,V1,M2} { convergent_lines( X, skol3 ), !
% 1.48/1.87 unorthogonal_lines( skol2, X ) }.
% 1.48/1.87 substitution0:
% 1.48/1.87 X := X
% 1.48/1.87 end
% 1.48/1.87 permutation0:
% 1.48/1.87 0 ==> 0
% 1.48/1.87 1 ==> 1
% 1.48/1.87 end
% 1.48/1.87
% 1.48/1.87 resolution: (5807) {G2,W12,D2,L4,V1,M4} { convergent_lines( skol3, skol3 )
% 1.48/1.87 , ! distinct_lines( skol2, skol1 ), apart_point_and_line( X, skol2 ),
% 1.48/1.87 apart_point_and_line( X, skol1 ) }.
% 1.48/1.87 parent0[1]: (5015) {G4,W6,D2,L2,V1,M1} R(183,28);r(61) { convergent_lines(
% 1.48/1.87 X, skol3 ), ! unorthogonal_lines( skol2, X ) }.
% 1.48/1.87 parent1[3]: (250) {G1,W12,D2,L4,V2,M1} R(25,27) { ! distinct_lines( X,
% 1.48/1.87 skol1 ), apart_point_and_line( Y, X ), apart_point_and_line( Y, skol1 ),
% 1.48/1.87 unorthogonal_lines( X, skol3 ) }.
% 1.48/1.87 substitution0:
% 1.48/1.87 X := skol3
% 1.48/1.87 end
% 1.48/1.87 substitution1:
% 1.48/1.87 X := skol2
% 1.48/1.87 Y := X
% 1.48/1.87 end
% 1.48/1.87
% 1.48/1.87 resolution: (5808) {G1,W9,D2,L3,V1,M3} { ! distinct_lines( skol2, skol1 )
% 1.48/1.87 , apart_point_and_line( X, skol2 ), apart_point_and_line( X, skol1 ) }.
% 1.48/1.87 parent0[0]: (2) {G0,W3,D2,L1,V1,M1} I { ! convergent_lines( X, X ) }.
% 1.48/1.87 parent1[0]: (5807) {G2,W12,D2,L4,V1,M4} { convergent_lines( skol3, skol3 )
% 1.48/1.87 , ! distinct_lines( skol2, skol1 ), apart_point_and_line( X, skol2 ),
% 1.48/1.87 apart_point_and_line( X, skol1 ) }.
% 1.48/1.87 substitution0:
% 1.48/1.87 X := skol3
% 1.48/1.87 end
% 1.48/1.87 substitution1:
% 1.48/1.87 X := X
% 1.48/1.87 end
% 1.48/1.87
% 1.48/1.87 subsumption: (5121) {G5,W9,D2,L3,V1,M1} R(250,5015);r(2) { ! distinct_lines
% 1.48/1.87 ( skol2, skol1 ), apart_point_and_line( X, skol1 ), apart_point_and_line
% 1.48/1.87 ( X, skol2 ) }.
% 1.48/1.87 parent0: (5808) {G1,W9,D2,L3,V1,M3} { ! distinct_lines( skol2, skol1 ),
% 1.48/1.87 apart_point_and_line( X, skol2 ), apart_point_and_line( X, skol1 ) }.
% 1.48/1.87 substitution0:
% 1.48/1.87 X := X
% 1.48/1.87 end
% 1.48/1.87 permutation0:
% 1.48/1.87 0 ==> 0
% 1.48/1.87 1 ==> 2
% 1.48/1.87 2 ==> 1
% 1.48/1.87 end
% 1.48/1.87
% 1.48/1.87 resolution: (5810) {G1,W11,D3,L3,V1,M3} { ! convergent_lines( X, skol2 ),
% 1.48/1.87 ! distinct_lines( skol2, skol1 ), apart_point_and_line(
% 1.48/1.87 intersection_point( X, skol2 ), skol1 ) }.
% 1.48/1.87 parent0[1]: (9) {G0,W8,D3,L2,V2,M1} I { ! convergent_lines( X, Y ), !
% 1.48/1.87 apart_point_and_line( intersection_point( X, Y ), Y ) }.
% 1.48/1.87 parent1[2]: (5121) {G5,W9,D2,L3,V1,M1} R(250,5015);r(2) { ! distinct_lines
% 1.48/1.87 ( skol2, skol1 ), apart_point_and_line( X, skol1 ), apart_point_and_line
% 1.48/1.87 ( X, skol2 ) }.
% 1.48/1.87 substitution0:
% 1.48/1.87 X := X
% 1.48/1.87 Y := skol2
% 1.48/1.87 end
% 1.48/1.87 substitution1:
% 1.48/1.87 X := intersection_point( X, skol2 )
% 1.48/1.87 end
% 1.48/1.87
% 1.48/1.87 subsumption: (5327) {G6,W11,D3,L3,V1,M1} R(5121,9) { ! distinct_lines(
% 1.48/1.87 skol2, skol1 ), ! convergent_lines( X, skol2 ), apart_point_and_line(
% 1.48/1.87 intersection_point( X, skol2 ), skol1 ) }.
% 1.48/1.87 parent0: (5810) {G1,W11,D3,L3,V1,M3} { ! convergent_lines( X, skol2 ), !
% 1.48/1.87 distinct_lines( skol2, skol1 ), apart_point_and_line( intersection_point
% 1.48/1.87 ( X, skol2 ), skol1 ) }.
% 1.48/1.87 substitution0:
% 1.48/1.87 X := X
% 1.48/1.87 end
% 1.48/1.87 permutation0:
% 1.48/1.87 0 ==> 1
% 1.48/1.87 1 ==> 0
% 1.48/1.87 2 ==> 2
% 1.48/1.87 end
% 1.48/1.87
% 1.48/1.87 resolution: (5811) {G1,W9,D2,L3,V0,M3} { ! convergent_lines( skol1, skol2
% 1.48/1.87 ), ! distinct_lines( skol2, skol1 ), ! convergent_lines( skol1, skol2 )
% 1.48/1.87 }.
% 1.48/1.87 parent0[1]: (8) {G0,W8,D3,L2,V2,M1} I { ! convergent_lines( X, Y ), !
% 1.48/1.87 apart_point_and_line( intersection_point( X, Y ), X ) }.
% 1.48/1.87 parent1[2]: (5327) {G6,W11,D3,L3,V1,M1} R(5121,9) { ! distinct_lines( skol2
% 1.48/1.87 , skol1 ), ! convergent_lines( X, skol2 ), apart_point_and_line(
% 1.48/1.87 intersection_point( X, skol2 ), skol1 ) }.
% 1.48/1.87 substitution0:
% 1.48/1.87 X := skol1
% 1.48/1.87 Y := skol2
% 1.48/1.87 end
% 1.48/1.87 substitution1:
% 1.48/1.87 X := skol1
% 1.48/1.87 end
% 1.48/1.87
% 1.48/1.87 factor: (5812) {G1,W6,D2,L2,V0,M2} { ! convergent_lines( skol1, skol2 ), !
% 1.48/1.87 distinct_lines( skol2, skol1 ) }.
% 1.48/1.87 parent0[0, 2]: (5811) {G1,W9,D2,L3,V0,M3} { ! convergent_lines( skol1,
% 1.48/1.87 skol2 ), ! distinct_lines( skol2, skol1 ), ! convergent_lines( skol1,
% 1.48/1.87 skol2 ) }.
% 1.48/1.87 substitution0:
% 1.48/1.87 end
% 1.48/1.87
% 1.48/1.87 resolution: (5814) {G1,W3,D2,L1,V0,M1} { ! distinct_lines( skol2, skol1 )
% 1.48/1.87 }.
% 1.48/1.87 parent0[0]: (5812) {G1,W6,D2,L2,V0,M2} { ! convergent_lines( skol1, skol2
% 1.48/1.87 ), ! distinct_lines( skol2, skol1 ) }.
% 1.48/1.87 parent1[0]: (26) {G0,W3,D2,L1,V0,M1} I { convergent_lines( skol1, skol2 )
% 1.48/1.87 }.
% 1.48/1.87 substitution0:
% 1.48/1.87 end
% 1.48/1.87 substitution1:
% 1.48/1.87 end
% 1.48/1.87
% 1.48/1.87 subsumption: (5526) {G7,W3,D2,L1,V0,M1} R(5327,8);f;r(26) { !
% 1.48/1.87 distinct_lines( skol2, skol1 ) }.
% 1.48/1.87 parent0: (5814) {G1,W3,D2,L1,V0,M1} { ! distinct_lines( skol2, skol1 ) }.
% 1.48/1.87 substitution0:
% 1.48/1.87 end
% 1.48/1.87 permutation0:
% 1.48/1.87 0 ==> 0
% 1.48/1.87 end
% 1.48/1.87
% 1.48/1.87 resolution: (5815) {G3,W6,D2,L2,V1,M2} { ! convergent_lines( X, skol1 ),
% 1.48/1.87 convergent_lines( X, skol2 ) }.
% 1.48/1.87 parent0[0]: (5526) {G7,W3,D2,L1,V0,M1} R(5327,8);f;r(26) { ! distinct_lines
% 1.48/1.87 ( skol2, skol1 ) }.
% 1.48/1.87 parent1[2]: (145) {G2,W9,D2,L3,V3,M1} R(13,34) { ! convergent_lines( X, Y )
% 1.48/1.87 , convergent_lines( X, Z ), distinct_lines( Z, Y ) }.
% 1.48/1.87 substitution0:
% 1.48/1.87 end
% 1.48/1.87 substitution1:
% 1.48/1.87 X := X
% 1.48/1.87 Y := skol1
% 1.48/1.87 Z := skol2
% 1.48/1.87 end
% 1.48/1.87
% 1.48/1.87 resolution: (5816) {G4,W6,D2,L2,V1,M2} { convergent_lines( X, skol2 ),
% 1.48/1.87 convergent_lines( X, skol2 ) }.
% 1.48/1.87 parent0[0]: (5815) {G3,W6,D2,L2,V1,M2} { ! convergent_lines( X, skol1 ),
% 1.48/1.87 convergent_lines( X, skol2 ) }.
% 1.48/1.87 parent1[0]: (141) {G3,W6,D2,L2,V1,M1} R(124,44) { convergent_lines( X,
% 1.48/1.87 skol1 ), convergent_lines( X, skol2 ) }.
% 1.48/1.87 substitution0:
% 1.48/1.87 X := X
% 1.48/1.87 end
% 1.48/1.87 substitution1:
% 1.48/1.87 X := X
% 1.48/1.87 end
% 1.48/1.87
% 1.48/1.87 factor: (5817) {G4,W3,D2,L1,V1,M1} { convergent_lines( X, skol2 ) }.
% 1.48/1.87 parent0[0, 1]: (5816) {G4,W6,D2,L2,V1,M2} { convergent_lines( X, skol2 ),
% 1.48/1.87 convergent_lines( X, skol2 ) }.
% 1.48/1.87 substitution0:
% 1.48/1.87 X := X
% 1.48/1.87 end
% 1.48/1.87
% 1.48/1.87 subsumption: (5605) {G8,W3,D2,L1,V1,M1} R(5526,145);r(141) {
% 1.48/1.87 convergent_lines( X, skol2 ) }.
% 1.48/1.87 parent0: (5817) {G4,W3,D2,L1,V1,M1} { convergent_lines( X, skol2 ) }.
% 1.48/1.87 substitution0:
% 1.48/1.87 X := X
% 1.48/1.87 end
% 1.48/1.87 permutation0:
% 1.48/1.87 0 ==> 0
% 1.48/1.87 end
% 1.48/1.87
% 1.48/1.87 resolution: (5818) {G7,W0,D0,L0,V0,M0} { }.
% 1.48/1.87 parent0[0]: (346) {G6,W9,D5,L1,V4,M1} R(343,244) { ! convergent_lines(
% 1.48/1.87 parallel_through_point( parallel_through_point( parallel_through_point( X
% 1.48/1.87 , Y ), Z ), T ), X ) }.
% 1.48/1.87 parent1[0]: (5605) {G8,W3,D2,L1,V1,M1} R(5526,145);r(141) {
% 1.48/1.87 convergent_lines( X, skol2 ) }.
% 1.48/1.87 substitution0:
% 1.48/1.87 X := skol2
% 1.48/1.87 Y := X
% 1.48/1.87 Z := Y
% 1.48/1.87 T := Z
% 1.48/1.87 end
% 1.48/1.87 substitution1:
% 1.48/1.87 X := parallel_through_point( parallel_through_point(
% 1.48/1.87 parallel_through_point( skol2, X ), Y ), Z )
% 1.48/1.87 end
% 1.48/1.87
% 1.48/1.87 subsumption: (5639) {G9,W0,D0,L0,V0,M0} R(5605,346) { }.
% 1.48/1.87 parent0: (5818) {G7,W0,D0,L0,V0,M0} { }.
% 1.48/1.87 substitution0:
% 1.48/1.87 end
% 1.48/1.87 permutation0:
% 1.48/1.87 end
% 1.48/1.87
% 1.48/1.87 Proof check complete!
% 1.48/1.87
% 1.48/1.87 Memory use:
% 1.48/1.87
% 1.48/1.87 space for terms: 78188
% 1.48/1.87 space for clauses: 211284
% 1.48/1.87
% 1.48/1.87
% 1.48/1.87 clauses generated: 78696
% 1.48/1.87 clauses kept: 5640
% 1.48/1.87 clauses selected: 820
% 1.48/1.87 clauses deleted: 9
% 1.48/1.87 clauses inuse deleted: 0
% 1.48/1.87
% 1.48/1.87 subsentry: 994587
% 1.48/1.87 literals s-matched: 432796
% 1.48/1.87 literals matched: 432751
% 1.48/1.87 full subsumption: 232246
% 1.48/1.87
% 1.48/1.87 checksum: 888055476
% 1.48/1.87
% 1.48/1.87
% 1.48/1.87 Bliksem ended
%------------------------------------------------------------------------------