%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : GEO223+2 : TPTP v8.1.0. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n006.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:59 EDT 2022
% Result : Theorem 101.23s 101.60s
% Output : Refutation 101.23s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.13 % Problem : GEO223+2 : TPTP v8.1.0. Released v3.3.0.
% 0.03/0.13 % Command : bliksem %s
% 0.14/0.35 % Computer : n006.cluster.edu
% 0.14/0.35 % Model : x86_64 x86_64
% 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35 % Memory : 8042.1875MB
% 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.35 % CPULimit : 300
% 0.14/0.35 % DateTime : Sat Jun 18 06:27:25 EDT 2022
% 0.14/0.35 % CPUTime :
% 101.23/101.59 *** allocated 10000 integers for termspace/termends
% 101.23/101.59 *** allocated 10000 integers for clauses
% 101.23/101.59 *** allocated 10000 integers for justifications
% 101.23/101.59 Bliksem 1.12
% 101.23/101.59
% 101.23/101.59
% 101.23/101.59 Automatic Strategy Selection
% 101.23/101.59
% 101.23/101.59
% 101.23/101.59 Clauses:
% 101.23/101.59
% 101.23/101.59 { ! distinct_points( X, X ) }.
% 101.23/101.59 { ! distinct_lines( X, X ) }.
% 101.23/101.59 { ! convergent_lines( X, X ) }.
% 101.23/101.59 { ! distinct_points( X, Y ), distinct_points( X, Z ), distinct_points( Y, Z
% 101.23/101.59 ) }.
% 101.23/101.59 { ! distinct_lines( X, Y ), distinct_lines( X, Z ), distinct_lines( Y, Z )
% 101.23/101.59 }.
% 101.23/101.59 { ! convergent_lines( X, Y ), convergent_lines( X, Z ), convergent_lines( Y
% 101.23/101.59 , Z ) }.
% 101.23/101.59 { ! distinct_points( X, Y ), ! apart_point_and_line( Z, line_connecting( X
% 101.23/101.59 , Y ) ), distinct_points( Z, X ) }.
% 101.23/101.59 { ! distinct_points( X, Y ), ! apart_point_and_line( Z, line_connecting( X
% 101.23/101.59 , Y ) ), distinct_points( Z, Y ) }.
% 101.23/101.59 { ! convergent_lines( X, Y ), ! apart_point_and_line( Z, X ),
% 101.23/101.59 distinct_points( Z, intersection_point( X, Y ) ) }.
% 101.23/101.59 { ! convergent_lines( X, Y ), ! apart_point_and_line( Z, Y ),
% 101.23/101.59 distinct_points( Z, intersection_point( X, Y ) ) }.
% 101.23/101.59 { ! distinct_points( X, Y ), ! distinct_lines( Z, T ), apart_point_and_line
% 101.23/101.59 ( X, Z ), apart_point_and_line( X, T ), apart_point_and_line( Y, Z ),
% 101.23/101.59 apart_point_and_line( Y, T ) }.
% 101.23/101.59 { ! apart_point_and_line( X, Y ), distinct_points( X, Z ),
% 101.23/101.59 apart_point_and_line( Z, Y ) }.
% 101.23/101.59 { ! apart_point_and_line( X, Y ), distinct_lines( Y, Z ),
% 101.23/101.59 apart_point_and_line( X, Z ) }.
% 101.23/101.59 { ! convergent_lines( X, Y ), distinct_lines( X, Y ) }.
% 101.23/101.59 { ! convergent_lines( parallel_through_point( Y, X ), Y ) }.
% 101.23/101.59 { ! apart_point_and_line( X, parallel_through_point( Y, X ) ) }.
% 101.23/101.59 { ! distinct_lines( X, Y ), apart_point_and_line( Z, X ),
% 101.23/101.59 apart_point_and_line( Z, Y ), convergent_lines( X, Y ) }.
% 101.23/101.59 { convergent_lines( X, Y ), unorthogonal_lines( X, Y ) }.
% 101.23/101.59 { ! convergent_lines( X, Y ), ! unorthogonal_lines( X, Y ), alpha1( X, Z )
% 101.23/101.59 , convergent_lines( Y, Z ) }.
% 101.23/101.59 { ! convergent_lines( X, Y ), ! unorthogonal_lines( X, Y ), alpha1( X, Z )
% 101.23/101.59 , unorthogonal_lines( Y, Z ) }.
% 101.23/101.59 { ! alpha1( X, Y ), convergent_lines( X, Y ) }.
% 101.23/101.59 { ! alpha1( X, Y ), unorthogonal_lines( X, Y ) }.
% 101.23/101.59 { ! convergent_lines( X, Y ), ! unorthogonal_lines( X, Y ), alpha1( X, Y )
% 101.23/101.59 }.
% 101.23/101.59 { ! unorthogonal_lines( orthogonal_through_point( Y, X ), Y ) }.
% 101.23/101.59 { ! apart_point_and_line( X, orthogonal_through_point( Y, X ) ) }.
% 101.23/101.59 { ! distinct_lines( X, Y ), apart_point_and_line( Z, X ),
% 101.23/101.59 apart_point_and_line( Z, Y ), unorthogonal_lines( X, T ),
% 101.23/101.59 unorthogonal_lines( Y, T ) }.
% 101.23/101.59 { distinct_lines( parallel_through_point( skol2, skol1 ),
% 101.23/101.59 orthogonal_through_point( orthogonal_through_point( skol2, skol1 ), skol1
% 101.23/101.59 ) ) }.
% 101.23/101.59
% 101.23/101.59 percentage equality = 0.000000, percentage horn = 0.592593
% 101.23/101.59 This a non-horn, non-equality problem
% 101.23/101.59
% 101.23/101.59
% 101.23/101.59 Options Used:
% 101.23/101.59
% 101.23/101.59 useres = 1
% 101.23/101.59 useparamod = 0
% 101.23/101.59 useeqrefl = 0
% 101.23/101.59 useeqfact = 0
% 101.23/101.59 usefactor = 1
% 101.23/101.59 usesimpsplitting = 0
% 101.23/101.59 usesimpdemod = 0
% 101.23/101.59 usesimpres = 3
% 101.23/101.59
% 101.23/101.59 resimpinuse = 1000
% 101.23/101.59 resimpclauses = 20000
% 101.23/101.59 substype = standard
% 101.23/101.59 backwardsubs = 1
% 101.23/101.59 selectoldest = 5
% 101.23/101.59
% 101.23/101.59 litorderings [0] = split
% 101.23/101.59 litorderings [1] = liftord
% 101.23/101.59
% 101.23/101.59 termordering = none
% 101.23/101.59
% 101.23/101.59 litapriori = 1
% 101.23/101.59 termapriori = 0
% 101.23/101.59 litaposteriori = 0
% 101.23/101.59 termaposteriori = 0
% 101.23/101.59 demodaposteriori = 0
% 101.23/101.59 ordereqreflfact = 0
% 101.23/101.59
% 101.23/101.59 litselect = none
% 101.23/101.59
% 101.23/101.59 maxweight = 15
% 101.23/101.59 maxdepth = 30000
% 101.23/101.59 maxlength = 115
% 101.23/101.59 maxnrvars = 195
% 101.23/101.59 excuselevel = 1
% 101.23/101.59 increasemaxweight = 1
% 101.23/101.59
% 101.23/101.59 maxselected = 10000000
% 101.23/101.59 maxnrclauses = 10000000
% 101.23/101.59
% 101.23/101.59 showgenerated = 0
% 101.23/101.59 showkept = 0
% 101.23/101.59 showselected = 0
% 101.23/101.59 showdeleted = 0
% 101.23/101.59 showresimp = 1
% 101.23/101.59 showstatus = 2000
% 101.23/101.59
% 101.23/101.59 prologoutput = 0
% 101.23/101.59 nrgoals = 5000000
% 101.23/101.59 totalproof = 1
% 101.23/101.59
% 101.23/101.59 Symbols occurring in the translation:
% 101.23/101.59
% 101.23/101.59 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 101.23/101.59 . [1, 2] (w:1, o:22, a:1, s:1, b:0),
% 101.23/101.59 ! [4, 1] (w:0, o:17, a:1, s:1, b:0),
% 101.23/101.59 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 101.23/101.59 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 101.23/101.59 distinct_points [36, 2] (w:1, o:47, a:1, s:1, b:0),
% 101.23/101.59 distinct_lines [37, 2] (w:1, o:48, a:1, s:1, b:0),
% 101.23/101.59 convergent_lines [38, 2] (w:1, o:46, a:1, s:1, b:0),
% 101.23/101.59 line_connecting [41, 2] (w:1, o:49, a:1, s:1, b:0),
% 101.23/101.60 apart_point_and_line [42, 2] (w:1, o:50, a:1, s:1, b:0),
% 101.23/101.60 intersection_point [43, 2] (w:1, o:51, a:1, s:1, b:0),
% 101.23/101.60 parallel_through_point [46, 2] (w:1, o:53, a:1, s:1, b:0),
% 101.23/101.60 unorthogonal_lines [49, 2] (w:1, o:54, a:1, s:1, b:0),
% 101.23/101.60 orthogonal_through_point [52, 2] (w:1, o:52, a:1, s:1, b:0),
% 101.23/101.60 alpha1 [53, 2] (w:1, o:55, a:1, s:1, b:0),
% 101.23/101.60 skol1 [54, 0] (w:1, o:15, a:1, s:1, b:0),
% 101.23/101.60 skol2 [55, 0] (w:1, o:16, a:1, s:1, b:0).
% 101.23/101.60
% 101.23/101.60
% 101.23/101.60 Starting Search:
% 101.23/101.60
% 101.23/101.60 *** allocated 15000 integers for clauses
% 101.23/101.60 *** allocated 22500 integers for clauses
% 101.23/101.60 *** allocated 33750 integers for clauses
% 101.23/101.60 *** allocated 15000 integers for termspace/termends
% 101.23/101.60 *** allocated 50625 integers for clauses
% 101.23/101.60 Resimplifying inuse:
% 101.23/101.60 Done
% 101.23/101.60
% 101.23/101.60 *** allocated 22500 integers for termspace/termends
% 101.23/101.60 *** allocated 75937 integers for clauses
% 101.23/101.60 *** allocated 33750 integers for termspace/termends
% 101.23/101.60 *** allocated 113905 integers for clauses
% 101.23/101.60 Resimplifying inuse:
% 101.23/101.60 Done
% 101.23/101.60
% 101.23/101.60 Failed to find proof!
% 101.23/101.60 maxweight = 15
% 101.23/101.60 maxnrclauses = 10000000
% 101.23/101.60 Generated: 1578929
% 101.23/101.60 Kept: 1956
% 101.23/101.60
% 101.23/101.60
% 101.23/101.60 The strategy used was not complete!
% 101.23/101.60
% 101.23/101.60 Increased maxweight to 16
% 101.23/101.60
% 101.23/101.60 Starting Search:
% 101.23/101.60
% 101.23/101.60 Resimplifying inuse:
% 101.23/101.60 Done
% 101.23/101.60
% 101.23/101.60
% 101.23/101.60 Intermediate Status:
% 101.23/101.60 Generated: 16599
% 101.23/101.60 Kept: 2012
% 101.23/101.60 Inuse: 209
% 101.23/101.60 Deleted: 0
% 101.23/101.60 Deletedinuse: 0
% 101.23/101.60
% 101.23/101.60 Resimplifying inuse:
% 101.23/101.60 Done
% 101.23/101.60
% 101.23/101.60 *** allocated 50625 integers for termspace/termends
% 101.23/101.60 *** allocated 170857 integers for clauses
% 101.23/101.60 Resimplifying inuse:
% 101.23/101.60 Done
% 101.23/101.60
% 101.23/101.60 *** allocated 75937 integers for termspace/termends
% 101.23/101.60 Resimplifying inuse:
% 101.23/101.60 Done
% 101.23/101.60
% 101.23/101.60 Failed to find proof!
% 101.23/101.60 maxweight = 16
% 101.23/101.60 maxnrclauses = 10000000
% 101.23/101.60 Generated: 4889972
% 101.23/101.60 Kept: 3486
% 101.23/101.60
% 101.23/101.60
% 101.23/101.60 The strategy used was not complete!
% 101.23/101.60
% 101.23/101.60 Increased maxweight to 17
% 101.23/101.60
% 101.23/101.60 Starting Search:
% 101.23/101.60
% 101.23/101.60 Resimplifying inuse:
% 101.23/101.60 Done
% 101.23/101.60
% 101.23/101.60
% 101.23/101.60 Intermediate Status:
% 101.23/101.60 Generated: 16274
% 101.23/101.60 Kept: 2019
% 101.23/101.60 Inuse: 195
% 101.23/101.60 Deleted: 0
% 101.23/101.60 Deletedinuse: 0
% 101.23/101.60
% 101.23/101.60 Resimplifying inuse:
% 101.23/101.60 Done
% 101.23/101.60
% 101.23/101.60 Resimplifying inuse:
% 101.23/101.60 Done
% 101.23/101.60
% 101.23/101.60
% 101.23/101.60 Intermediate Status:
% 101.23/101.60 Generated: 41044
% 101.23/101.60 Kept: 4027
% 101.23/101.60 Inuse: 362
% 101.23/101.60 Deleted: 1
% 101.23/101.60 Deletedinuse: 0
% 101.23/101.60
% 101.23/101.60 Resimplifying inuse:
% 101.23/101.60 Done
% 101.23/101.60
% 101.23/101.60 *** allocated 256285 integers for clauses
% 101.23/101.60 *** allocated 113905 integers for termspace/termends
% 101.23/101.60 Resimplifying inuse:
% 101.23/101.60 Done
% 101.23/101.60
% 101.23/101.60
% 101.23/101.60 Intermediate Status:
% 101.23/101.60 Generated: 6987092
% 101.23/101.60 Kept: 6144
% 101.23/101.60 Inuse: 3791
% 101.23/101.60 Deleted: 144
% 101.23/101.60 Deletedinuse: 5
% 101.23/101.60
% 101.23/101.60 Resimplifying inuse:
% 101.23/101.60 Done
% 101.23/101.60
% 101.23/101.60 *** allocated 384427 integers for clauses
% 101.23/101.60 *** allocated 170857 integers for termspace/termends
% 101.23/101.60 Resimplifying inuse:
% 101.23/101.60 Done
% 101.23/101.60
% 101.23/101.60
% 101.23/101.60 Intermediate Status:
% 101.23/101.60 Generated: 14873347
% 101.23/101.60 Kept: 8711
% 101.23/101.60 Inuse: 6536
% 101.23/101.60 Deleted: 332
% 101.23/101.60 Deletedinuse: 23
% 101.23/101.60
% 101.23/101.60 Resimplifying inuse:
% 101.23/101.60 Done
% 101.23/101.60
% 101.23/101.60 *** allocated 576640 integers for clauses
% 101.23/101.60 Resimplifying inuse:
% 101.23/101.60 Done
% 101.23/101.60
% 101.23/101.60 *** allocated 256285 integers for termspace/termends
% 101.23/101.60
% 101.23/101.60 Intermediate Status:
% 101.23/101.60 Generated: 15301234
% 101.23/101.60 Kept: 10719
% 101.23/101.60 Inuse: 6670
% 101.23/101.60 Deleted: 368
% 101.23/101.60 Deletedinuse: 24
% 101.23/101.60
% 101.23/101.60 Resimplifying inuse:
% 101.23/101.60 Done
% 101.23/101.60
% 101.23/101.60 Resimplifying inuse:
% 101.23/101.60
% 101.23/101.60 Bliksems!, er is een bewijs:
% 101.23/101.60 % SZS status Theorem
% 101.23/101.60 % SZS output start Refutation
% 101.23/101.60
% 101.23/101.60 (0) {G0,W3,D2,L1,V1,M1} I { ! distinct_points( X, X ) }.
% 101.23/101.60 (1) {G0,W3,D2,L1,V1,M1} I { ! distinct_lines( X, X ) }.
% 101.23/101.60 (2) {G0,W3,D2,L1,V1,M1} I { ! convergent_lines( X, X ) }.
% 101.23/101.60 (4) {G0,W9,D2,L3,V3,M3} I { distinct_lines( X, Z ), distinct_lines( Y, Z )
% 101.23/101.60 , ! distinct_lines( X, Y ) }.
% 101.23/101.60 (5) {G0,W9,D2,L3,V3,M3} I { convergent_lines( X, Z ), convergent_lines( Y,
% 101.23/101.60 Z ), ! convergent_lines( X, Y ) }.
% 101.23/101.60 (8) {G0,W11,D3,L3,V3,M1} I { ! convergent_lines( X, Y ), distinct_points( Z
% 101.23/101.60 , intersection_point( X, Y ) ), ! apart_point_and_line( Z, X ) }.
% 101.23/101.60 (9) {G0,W11,D3,L3,V3,M1} I { ! convergent_lines( X, Y ), distinct_points( Z
% 101.23/101.60 , intersection_point( X, Y ) ), ! apart_point_and_line( Z, Y ) }.
% 101.23/101.60 (11) {G0,W9,D2,L3,V3,M2} I { distinct_points( X, Z ), apart_point_and_line
% 101.23/101.60 ( Z, Y ), ! apart_point_and_line( X, Y ) }.
% 101.23/101.60 (12) {G0,W9,D2,L3,V3,M2} I { distinct_lines( Y, Z ), apart_point_and_line(
% 101.23/101.60 X, Z ), ! apart_point_and_line( X, Y ) }.
% 101.23/101.60 (13) {G0,W6,D2,L2,V2,M1} I { ! convergent_lines( X, Y ), distinct_lines( X
% 101.23/101.60 , Y ) }.
% 101.23/101.60 (14) {G0,W5,D3,L1,V2,M1} I { ! convergent_lines( parallel_through_point( Y
% 101.23/101.60 , X ), Y ) }.
% 101.23/101.60 (15) {G0,W5,D3,L1,V2,M1} I { ! apart_point_and_line( X,
% 101.23/101.60 parallel_through_point( Y, X ) ) }.
% 101.23/101.60 (16) {G0,W12,D2,L4,V3,M2} I { ! distinct_lines( X, Y ), convergent_lines( X
% 101.23/101.60 , Y ), apart_point_and_line( Z, X ), apart_point_and_line( Z, Y ) }.
% 101.23/101.60 (17) {G0,W6,D2,L2,V2,M1} I { convergent_lines( X, Y ), unorthogonal_lines(
% 101.23/101.60 X, Y ) }.
% 101.23/101.60 (18) {G0,W12,D2,L4,V3,M1} I { ! convergent_lines( X, Y ), !
% 101.23/101.60 unorthogonal_lines( X, Y ), convergent_lines( Y, Z ), alpha1( X, Z ) }.
% 101.23/101.60 (19) {G0,W12,D2,L4,V3,M1} I { ! convergent_lines( X, Y ), !
% 101.23/101.60 unorthogonal_lines( X, Y ), unorthogonal_lines( Y, Z ), alpha1( X, Z )
% 101.23/101.60 }.
% 101.23/101.60 (20) {G0,W6,D2,L2,V2,M1} I { convergent_lines( X, Y ), ! alpha1( X, Y ) }.
% 101.23/101.60 (21) {G0,W6,D2,L2,V2,M1} I { unorthogonal_lines( X, Y ), ! alpha1( X, Y )
% 101.23/101.60 }.
% 101.23/101.60 (23) {G0,W5,D3,L1,V2,M1} I { ! unorthogonal_lines( orthogonal_through_point
% 101.23/101.60 ( Y, X ), Y ) }.
% 101.23/101.60 (24) {G0,W5,D3,L1,V2,M1} I { ! apart_point_and_line( X,
% 101.23/101.60 orthogonal_through_point( Y, X ) ) }.
% 101.23/101.60 (25) {G0,W15,D2,L5,V4,M2} I { ! distinct_lines( X, Y ),
% 101.23/101.60 apart_point_and_line( Z, X ), apart_point_and_line( Z, Y ),
% 101.23/101.60 unorthogonal_lines( Y, T ), unorthogonal_lines( X, T ) }.
% 101.23/101.60 (26) {G0,W9,D4,L1,V0,M1} I { distinct_lines( parallel_through_point( skol2
% 101.23/101.60 , skol1 ), orthogonal_through_point( orthogonal_through_point( skol2,
% 101.23/101.60 skol1 ), skol1 ) ) }.
% 101.23/101.60 (34) {G1,W6,D2,L2,V2,M2} R(4,1) { ! distinct_lines( Y, X ), distinct_lines
% 101.23/101.60 ( X, Y ) }.
% 101.23/101.60 (37) {G1,W5,D3,L1,V2,M1} R(17,23) { convergent_lines(
% 101.23/101.60 orthogonal_through_point( X, Y ), X ) }.
% 101.23/101.60 (40) {G2,W8,D3,L2,V3,M2} R(5,37) { convergent_lines( X, Z ),
% 101.23/101.60 convergent_lines( orthogonal_through_point( X, Y ), Z ) }.
% 101.23/101.60 (41) {G1,W8,D3,L2,V3,M2} R(5,14) { ! convergent_lines(
% 101.23/101.60 parallel_through_point( Y, Z ), X ), convergent_lines( X, Y ) }.
% 101.23/101.60 (43) {G1,W6,D2,L2,V2,M2} R(5,2) { ! convergent_lines( Y, X ),
% 101.23/101.60 convergent_lines( X, Y ) }.
% 101.23/101.60 (45) {G2,W9,D2,L3,V3,M3} R(43,5) { convergent_lines( Z, X ), !
% 101.23/101.60 convergent_lines( Z, Y ), convergent_lines( X, Y ) }.
% 101.23/101.60 (46) {G2,W5,D3,L1,V2,M1} R(43,37) { convergent_lines( X,
% 101.23/101.60 orthogonal_through_point( X, Y ) ) }.
% 101.23/101.60 (93) {G3,W8,D3,L2,V3,M2} R(40,43) { convergent_lines( Z, X ),
% 101.23/101.60 convergent_lines( orthogonal_through_point( X, Y ), Z ) }.
% 101.23/101.60 (151) {G2,W11,D3,L3,V4,M3} R(41,5) { convergent_lines( Z, X ), !
% 101.23/101.60 convergent_lines( Z, parallel_through_point( Y, T ) ), convergent_lines(
% 101.23/101.60 X, Y ) }.
% 101.23/101.60 (167) {G1,W14,D3,L4,V4,M1} R(11,9) { distinct_points( X, Y ), !
% 101.23/101.60 convergent_lines( T, Z ), distinct_points( Y, intersection_point( T, Z )
% 101.23/101.60 ), ! apart_point_and_line( X, Z ) }.
% 101.23/101.60 (168) {G1,W14,D3,L4,V4,M1} R(11,8) { distinct_points( X, Y ), !
% 101.23/101.60 convergent_lines( Z, T ), distinct_points( Y, intersection_point( Z, T )
% 101.23/101.60 ), ! apart_point_and_line( X, Z ) }.
% 101.23/101.60 (175) {G2,W8,D3,L2,V2,M1} F(168);r(0) { ! convergent_lines( X, Y ), !
% 101.23/101.60 apart_point_and_line( intersection_point( X, Y ), X ) }.
% 101.23/101.60 (176) {G2,W8,D3,L2,V2,M1} F(167);r(0) { ! convergent_lines( X, Y ), !
% 101.23/101.60 apart_point_and_line( intersection_point( X, Y ), Y ) }.
% 101.23/101.60 (196) {G1,W8,D3,L2,V3,M1} R(12,24) { distinct_lines( X,
% 101.23/101.60 orthogonal_through_point( Y, Z ) ), ! apart_point_and_line( Z, X ) }.
% 101.23/101.60 (198) {G2,W11,D3,L3,V4,M1} R(196,12) { distinct_lines( X,
% 101.23/101.60 orthogonal_through_point( Y, Z ) ), distinct_lines( T, X ), !
% 101.23/101.60 apart_point_and_line( Z, T ) }.
% 101.23/101.60 (226) {G1,W13,D3,L3,V3,M1} R(16,15) { convergent_lines( X,
% 101.23/101.60 parallel_through_point( Y, Z ) ), ! distinct_lines( X,
% 101.23/101.60 parallel_through_point( Y, Z ) ), apart_point_and_line( Z, X ) }.
% 101.23/101.60 (241) {G1,W12,D2,L4,V3,M2} R(18,21) { ! convergent_lines( X, Y ),
% 101.23/101.60 convergent_lines( Y, Z ), unorthogonal_lines( X, Z ), !
% 101.23/101.60 unorthogonal_lines( X, Y ) }.
% 101.23/101.60 (264) {G1,W12,D2,L4,V3,M2} R(19,20) { ! convergent_lines( X, Y ),
% 101.23/101.60 convergent_lines( X, Z ), ! unorthogonal_lines( X, Y ),
% 101.23/101.60 unorthogonal_lines( Y, Z ) }.
% 101.23/101.60 (299) {G1,W16,D3,L4,V4,M1} R(25,23) { ! distinct_lines( X,
% 101.23/101.60 orthogonal_through_point( Y, Z ) ), apart_point_and_line( T, X ),
% 101.23/101.60 apart_point_and_line( T, orthogonal_through_point( Y, Z ) ),
% 101.23/101.60 unorthogonal_lines( X, Y ) }.
% 101.23/101.60 (300) {G1,W16,D3,L4,V4,M1} R(25,23) { ! distinct_lines(
% 101.23/101.60 orthogonal_through_point( X, Y ), Z ), apart_point_and_line( T,
% 101.23/101.60 orthogonal_through_point( X, Y ) ), apart_point_and_line( T, Z ),
% 101.23/101.60 unorthogonal_lines( Z, X ) }.
% 101.23/101.60 (318) {G2,W9,D4,L1,V0,M1} R(26,34) { distinct_lines(
% 101.23/101.60 orthogonal_through_point( orthogonal_through_point( skol2, skol1 ), skol1
% 101.23/101.60 ), parallel_through_point( skol2, skol1 ) ) }.
% 101.23/101.60 (1826) {G3,W14,D3,L4,V5,M1} R(198,12) { distinct_lines( X,
% 101.23/101.60 orthogonal_through_point( Y, Z ) ), distinct_lines( T, X ),
% 101.23/101.60 distinct_lines( U, T ), ! apart_point_and_line( Z, U ) }.
% 101.23/101.60 (1828) {G4,W8,D3,L2,V3,M1} F(1826);r(34) { distinct_lines(
% 101.23/101.60 orthogonal_through_point( Y, Z ), X ), ! apart_point_and_line( Z, X ) }.
% 101.23/101.60 (2975) {G4,W8,D3,L2,V3,M1} R(241,23);r(93) { convergent_lines( Z, X ), !
% 101.23/101.60 unorthogonal_lines( orthogonal_through_point( X, Y ), Z ) }.
% 101.23/101.60 (2979) {G5,W16,D3,L4,V4,M1} R(2975,264) { convergent_lines( X, Y ), !
% 101.23/101.60 convergent_lines( Z, orthogonal_through_point( Y, T ) ), convergent_lines
% 101.23/101.60 ( Z, X ), ! unorthogonal_lines( Z, orthogonal_through_point( Y, T ) ) }.
% 101.23/101.60 (2980) {G6,W10,D3,L2,V2,M1} F(2979);r(2) { ! convergent_lines( X,
% 101.23/101.60 orthogonal_through_point( X, Y ) ), ! unorthogonal_lines( X,
% 101.23/101.60 orthogonal_through_point( X, Y ) ) }.
% 101.23/101.60 (2981) {G7,W5,D3,L1,V2,M1} S(2980);r(46) { ! unorthogonal_lines( X,
% 101.23/101.60 orthogonal_through_point( X, Y ) ) }.
% 101.23/101.60 (4470) {G2,W14,D3,L2,V3,M1} R(226,24) { convergent_lines(
% 101.23/101.60 orthogonal_through_point( X, Y ), parallel_through_point( Z, Y ) ), !
% 101.23/101.60 distinct_lines( orthogonal_through_point( X, Y ), parallel_through_point
% 101.23/101.60 ( Z, Y ) ) }.
% 101.23/101.60 (4483) {G2,W17,D3,L3,V4,M2} R(299,23) { ! distinct_lines(
% 101.23/101.60 orthogonal_through_point( X, Y ), orthogonal_through_point( X, Z ) ),
% 101.23/101.60 apart_point_and_line( T, orthogonal_through_point( X, Z ) ),
% 101.23/101.60 apart_point_and_line( T, orthogonal_through_point( X, Y ) ) }.
% 101.23/101.60 (4484) {G8,W17,D4,L3,V4,M2} R(300,2981) { ! distinct_lines(
% 101.23/101.60 orthogonal_through_point( orthogonal_through_point( X, Y ), Z ), X ),
% 101.23/101.60 apart_point_and_line( T, X ), apart_point_and_line( T,
% 101.23/101.60 orthogonal_through_point( orthogonal_through_point( X, Y ), Z ) ) }.
% 101.23/101.60 (4893) {G3,W9,D4,L1,V0,M1} R(4470,318) { convergent_lines(
% 101.23/101.60 orthogonal_through_point( orthogonal_through_point( skol2, skol1 ), skol1
% 101.23/101.60 ), parallel_through_point( skol2, skol1 ) ) }.
% 101.23/101.60 (4979) {G4,W10,D4,L2,V1,M2} R(4893,151) { convergent_lines( X, skol2 ),
% 101.23/101.60 convergent_lines( orthogonal_through_point( orthogonal_through_point(
% 101.23/101.60 skol2, skol1 ), skol1 ), X ) }.
% 101.23/101.60 (5959) {G3,W12,D3,L2,V3,M1} R(4483,24) { ! distinct_lines(
% 101.23/101.60 orthogonal_through_point( X, Y ), orthogonal_through_point( X, Z ) ),
% 101.23/101.60 apart_point_and_line( Y, orthogonal_through_point( X, Z ) ) }.
% 101.23/101.60 (6189) {G5,W14,D3,L2,V4,M2} R(5959,1828) { distinct_lines(
% 101.23/101.60 orthogonal_through_point( T, Y ), orthogonal_through_point( X, Z ) ), !
% 101.23/101.60 distinct_lines( orthogonal_through_point( X, Y ),
% 101.23/101.60 orthogonal_through_point( X, Z ) ) }.
% 101.23/101.60 (6192) {G4,W16,D5,L2,V3,M1} R(5959,176) { ! convergent_lines( Y,
% 101.23/101.60 orthogonal_through_point( X, Z ) ), ! distinct_lines(
% 101.23/101.60 orthogonal_through_point( X, intersection_point( Y,
% 101.23/101.60 orthogonal_through_point( X, Z ) ) ), orthogonal_through_point( X, Z ) )
% 101.23/101.60 }.
% 101.23/101.60 (6301) {G6,W14,D3,L2,V4,M1} R(6189,13) { ! convergent_lines(
% 101.23/101.60 orthogonal_through_point( Z, Y ), orthogonal_through_point( Z, T ) ),
% 101.23/101.60 distinct_lines( orthogonal_through_point( X, Y ),
% 101.23/101.60 orthogonal_through_point( Z, T ) ) }.
% 101.23/101.60 (6346) {G7,W14,D3,L2,V4,M1} R(6301,34) { ! convergent_lines(
% 101.23/101.60 orthogonal_through_point( X, Y ), orthogonal_through_point( X, Z ) ),
% 101.23/101.60 distinct_lines( orthogonal_through_point( X, Z ),
% 101.23/101.60 orthogonal_through_point( T, Y ) ) }.
% 101.23/101.60 (6984) {G8,W16,D5,L2,V3,M2} R(6192,6346) { ! convergent_lines(
% 101.23/101.60 orthogonal_through_point( Y, Z ), orthogonal_through_point( Y,
% 101.23/101.60 intersection_point( X, orthogonal_through_point( Y, Z ) ) ) ), !
% 101.23/101.60 convergent_lines( X, orthogonal_through_point( Y, Z ) ) }.
% 101.23/101.60 (7003) {G9,W11,D5,L1,V2,M1} R(6984,46) { ! convergent_lines(
% 101.23/101.60 orthogonal_through_point( X, Y ), orthogonal_through_point( X,
% 101.23/101.60 intersection_point( X, orthogonal_through_point( X, Y ) ) ) ) }.
% 101.23/101.60 (7004) {G9,W16,D5,L2,V3,M2} R(6984,43) { ! convergent_lines(
% 101.23/101.60 orthogonal_through_point( X, Y ), Z ), ! convergent_lines(
% 101.23/101.60 orthogonal_through_point( X, Y ), orthogonal_through_point( X,
% 101.23/101.60 intersection_point( Z, orthogonal_through_point( X, Y ) ) ) ) }.
% 101.23/101.60 (7036) {G10,W15,D6,L1,V0,M1} R(7003,4979) { convergent_lines(
% 101.23/101.60 orthogonal_through_point( orthogonal_through_point( skol2, skol1 ),
% 101.23/101.60 intersection_point( orthogonal_through_point( skol2, skol1 ),
% 101.23/101.60 orthogonal_through_point( orthogonal_through_point( skol2, skol1 ), skol1
% 101.23/101.60 ) ) ), skol2 ) }.
% 101.23/101.60 (7555) {G9,W10,D4,L2,V3,M1} R(4484,24) { ! distinct_lines(
% 101.23/101.60 orthogonal_through_point( orthogonal_through_point( X, Y ), Z ), X ),
% 101.23/101.60 apart_point_and_line( Z, X ) }.
% 101.23/101.60 (7603) {G10,W12,D4,L2,V4,M2} R(7555,1828) { distinct_lines(
% 101.23/101.60 orthogonal_through_point( T, Z ), X ), ! distinct_lines(
% 101.23/101.60 orthogonal_through_point( orthogonal_through_point( X, Y ), Z ), X ) }.
% 101.23/101.60 (7607) {G10,W12,D4,L2,V3,M1} R(7555,175) { ! convergent_lines( X, Z ), !
% 101.23/101.60 distinct_lines( orthogonal_through_point( orthogonal_through_point( X, Y
% 101.23/101.60 ), intersection_point( X, Z ) ), X ) }.
% 101.23/101.60 (9450) {G11,W12,D4,L2,V4,M1} R(7603,13) { ! convergent_lines(
% 101.23/101.60 orthogonal_through_point( orthogonal_through_point( Z, T ), Y ), Z ),
% 101.23/101.60 distinct_lines( orthogonal_through_point( X, Y ), Z ) }.
% 101.23/101.60 (11051) {G12,W12,D4,L2,V3,M2} R(7607,9450) { ! convergent_lines(
% 101.23/101.60 orthogonal_through_point( orthogonal_through_point( X, Z ),
% 101.23/101.60 intersection_point( X, Y ) ), X ), ! convergent_lines( X, Y ) }.
% 101.23/101.60 (11398) {G13,W12,D4,L2,V3,M2} R(11051,43) { ! convergent_lines( Z, X ), !
% 101.23/101.60 convergent_lines( orthogonal_through_point( orthogonal_through_point( X,
% 101.23/101.60 Y ), intersection_point( X, Z ) ), X ) }.
% 101.23/101.60 (11629) {G14,W15,D4,L3,V4,M3} R(11398,45) { convergent_lines( Z,
% 101.23/101.60 orthogonal_through_point( orthogonal_through_point( Y, T ),
% 101.23/101.60 intersection_point( Y, X ) ) ), ! convergent_lines( Z, Y ), !
% 101.23/101.60 convergent_lines( X, Y ) }.
% 101.23/101.60 (11646) {G15,W12,D4,L2,V3,M2} F(11629) { ! convergent_lines( X, Y ),
% 101.23/101.60 convergent_lines( X, orthogonal_through_point( orthogonal_through_point(
% 101.23/101.60 Y, Z ), intersection_point( Y, X ) ) ) }.
% 101.23/101.60 (11653) {G16,W7,D4,L1,V3,M1} R(11646,7004);f { ! convergent_lines(
% 101.23/101.60 orthogonal_through_point( orthogonal_through_point( X, Y ), Z ), X ) }.
% 101.23/101.60 (11790) {G17,W0,D0,L0,V0,M0} S(7036);r(11653) { }.
% 101.23/101.60
% 101.23/101.60
% 101.23/101.60 % SZS output end Refutation
% 101.23/101.60 found a proof!
% 101.23/101.60
% 101.23/101.60
% 101.23/101.60 Unprocessed initial clauses:
% 101.23/101.60
% 101.23/101.60 (11792) {G0,W3,D2,L1,V1,M1} { ! distinct_points( X, X ) }.
% 101.23/101.60 (11793) {G0,W3,D2,L1,V1,M1} { ! distinct_lines( X, X ) }.
% 101.23/101.60 (11794) {G0,W3,D2,L1,V1,M1} { ! convergent_lines( X, X ) }.
% 101.23/101.60 (11795) {G0,W9,D2,L3,V3,M3} { ! distinct_points( X, Y ), distinct_points(
% 101.23/101.60 X, Z ), distinct_points( Y, Z ) }.
% 101.23/101.60 (11796) {G0,W9,D2,L3,V3,M3} { ! distinct_lines( X, Y ), distinct_lines( X
% 101.23/101.60 , Z ), distinct_lines( Y, Z ) }.
% 101.23/101.60 (11797) {G0,W9,D2,L3,V3,M3} { ! convergent_lines( X, Y ), convergent_lines
% 101.23/101.60 ( X, Z ), convergent_lines( Y, Z ) }.
% 101.23/101.60 (11798) {G0,W11,D3,L3,V3,M3} { ! distinct_points( X, Y ), !
% 101.23/101.60 apart_point_and_line( Z, line_connecting( X, Y ) ), distinct_points( Z, X
% 101.23/101.60 ) }.
% 101.23/101.60 (11799) {G0,W11,D3,L3,V3,M3} { ! distinct_points( X, Y ), !
% 101.23/101.60 apart_point_and_line( Z, line_connecting( X, Y ) ), distinct_points( Z, Y
% 101.23/101.60 ) }.
% 101.23/101.60 (11800) {G0,W11,D3,L3,V3,M3} { ! convergent_lines( X, Y ), !
% 101.23/101.60 apart_point_and_line( Z, X ), distinct_points( Z, intersection_point( X,
% 101.23/101.60 Y ) ) }.
% 101.23/101.60 (11801) {G0,W11,D3,L3,V3,M3} { ! convergent_lines( X, Y ), !
% 101.23/101.60 apart_point_and_line( Z, Y ), distinct_points( Z, intersection_point( X,
% 101.23/101.60 Y ) ) }.
% 101.23/101.60 (11802) {G0,W18,D2,L6,V4,M6} { ! distinct_points( X, Y ), ! distinct_lines
% 101.23/101.60 ( Z, T ), apart_point_and_line( X, Z ), apart_point_and_line( X, T ),
% 101.23/101.60 apart_point_and_line( Y, Z ), apart_point_and_line( Y, T ) }.
% 101.23/101.60 (11803) {G0,W9,D2,L3,V3,M3} { ! apart_point_and_line( X, Y ),
% 101.23/101.60 distinct_points( X, Z ), apart_point_and_line( Z, Y ) }.
% 101.23/101.60 (11804) {G0,W9,D2,L3,V3,M3} { ! apart_point_and_line( X, Y ),
% 101.23/101.60 distinct_lines( Y, Z ), apart_point_and_line( X, Z ) }.
% 101.23/101.60 (11805) {G0,W6,D2,L2,V2,M2} { ! convergent_lines( X, Y ), distinct_lines(
% 101.23/101.60 X, Y ) }.
% 101.23/101.60 (11806) {G0,W5,D3,L1,V2,M1} { ! convergent_lines( parallel_through_point(
% 101.23/101.60 Y, X ), Y ) }.
% 101.23/101.60 (11807) {G0,W5,D3,L1,V2,M1} { ! apart_point_and_line( X,
% 101.23/101.60 parallel_through_point( Y, X ) ) }.
% 101.23/101.60 (11808) {G0,W12,D2,L4,V3,M4} { ! distinct_lines( X, Y ),
% 101.23/101.60 apart_point_and_line( Z, X ), apart_point_and_line( Z, Y ),
% 101.23/101.60 convergent_lines( X, Y ) }.
% 101.23/101.60 (11809) {G0,W6,D2,L2,V2,M2} { convergent_lines( X, Y ), unorthogonal_lines
% 101.23/101.60 ( X, Y ) }.
% 101.23/101.60 (11810) {G0,W12,D2,L4,V3,M4} { ! convergent_lines( X, Y ), !
% 101.23/101.60 unorthogonal_lines( X, Y ), alpha1( X, Z ), convergent_lines( Y, Z ) }.
% 101.23/101.60 (11811) {G0,W12,D2,L4,V3,M4} { ! convergent_lines( X, Y ), !
% 101.23/101.60 unorthogonal_lines( X, Y ), alpha1( X, Z ), unorthogonal_lines( Y, Z )
% 101.23/101.60 }.
% 101.23/101.60 (11812) {G0,W6,D2,L2,V2,M2} { ! alpha1( X, Y ), convergent_lines( X, Y )
% 101.23/101.60 }.
% 101.23/101.60 (11813) {G0,W6,D2,L2,V2,M2} { ! alpha1( X, Y ), unorthogonal_lines( X, Y )
% 101.23/101.60 }.
% 101.23/101.60 (11814) {G0,W9,D2,L3,V2,M3} { ! convergent_lines( X, Y ), !
% 101.23/101.60 unorthogonal_lines( X, Y ), alpha1( X, Y ) }.
% 101.23/101.60 (11815) {G0,W5,D3,L1,V2,M1} { ! unorthogonal_lines(
% 101.23/101.60 orthogonal_through_point( Y, X ), Y ) }.
% 101.23/101.60 (11816) {G0,W5,D3,L1,V2,M1} { ! apart_point_and_line( X,
% 101.23/101.60 orthogonal_through_point( Y, X ) ) }.
% 101.23/101.60 (11817) {G0,W15,D2,L5,V4,M5} { ! distinct_lines( X, Y ),
% 101.23/101.60 apart_point_and_line( Z, X ), apart_point_and_line( Z, Y ),
% 101.23/101.60 unorthogonal_lines( X, T ), unorthogonal_lines( Y, T ) }.
% 101.23/101.60 (11818) {G0,W9,D4,L1,V0,M1} { distinct_lines( parallel_through_point(
% 101.23/101.60 skol2, skol1 ), orthogonal_through_point( orthogonal_through_point( skol2
% 101.23/101.60 , skol1 ), skol1 ) ) }.
% 101.23/101.60
% 101.23/101.60
% 101.23/101.60 Total Proof:
% 101.23/101.60
% 101.23/101.60 subsumption: (0) {G0,W3,D2,L1,V1,M1} I { ! distinct_points( X, X ) }.
% 101.23/101.60 parent0: (11792) {G0,W3,D2,L1,V1,M1} { ! distinct_points( X, X ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := X
% 101.23/101.60 end
% 101.23/101.60 permutation0:
% 101.23/101.60 0 ==> 0
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 subsumption: (1) {G0,W3,D2,L1,V1,M1} I { ! distinct_lines( X, X ) }.
% 101.23/101.60 parent0: (11793) {G0,W3,D2,L1,V1,M1} { ! distinct_lines( X, X ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := X
% 101.23/101.60 end
% 101.23/101.60 permutation0:
% 101.23/101.60 0 ==> 0
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 subsumption: (2) {G0,W3,D2,L1,V1,M1} I { ! convergent_lines( X, X ) }.
% 101.23/101.60 parent0: (11794) {G0,W3,D2,L1,V1,M1} { ! convergent_lines( X, X ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := X
% 101.23/101.60 end
% 101.23/101.60 permutation0:
% 101.23/101.60 0 ==> 0
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 subsumption: (4) {G0,W9,D2,L3,V3,M3} I { distinct_lines( X, Z ),
% 101.23/101.60 distinct_lines( Y, Z ), ! distinct_lines( X, Y ) }.
% 101.23/101.60 parent0: (11796) {G0,W9,D2,L3,V3,M3} { ! distinct_lines( X, Y ),
% 101.23/101.60 distinct_lines( X, Z ), distinct_lines( Y, Z ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := X
% 101.23/101.60 Y := Y
% 101.23/101.60 Z := Z
% 101.23/101.60 end
% 101.23/101.60 permutation0:
% 101.23/101.60 0 ==> 2
% 101.23/101.60 1 ==> 0
% 101.23/101.60 2 ==> 1
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 subsumption: (5) {G0,W9,D2,L3,V3,M3} I { convergent_lines( X, Z ),
% 101.23/101.60 convergent_lines( Y, Z ), ! convergent_lines( X, Y ) }.
% 101.23/101.60 parent0: (11797) {G0,W9,D2,L3,V3,M3} { ! convergent_lines( X, Y ),
% 101.23/101.60 convergent_lines( X, Z ), convergent_lines( Y, Z ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := X
% 101.23/101.60 Y := Y
% 101.23/101.60 Z := Z
% 101.23/101.60 end
% 101.23/101.60 permutation0:
% 101.23/101.60 0 ==> 2
% 101.23/101.60 1 ==> 0
% 101.23/101.60 2 ==> 1
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 subsumption: (8) {G0,W11,D3,L3,V3,M1} I { ! convergent_lines( X, Y ),
% 101.23/101.60 distinct_points( Z, intersection_point( X, Y ) ), ! apart_point_and_line
% 101.23/101.60 ( Z, X ) }.
% 101.23/101.60 parent0: (11800) {G0,W11,D3,L3,V3,M3} { ! convergent_lines( X, Y ), !
% 101.23/101.60 apart_point_and_line( Z, X ), distinct_points( Z, intersection_point( X,
% 101.23/101.60 Y ) ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := X
% 101.23/101.60 Y := Y
% 101.23/101.60 Z := Z
% 101.23/101.60 end
% 101.23/101.60 permutation0:
% 101.23/101.60 0 ==> 0
% 101.23/101.60 1 ==> 2
% 101.23/101.60 2 ==> 1
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 subsumption: (9) {G0,W11,D3,L3,V3,M1} I { ! convergent_lines( X, Y ),
% 101.23/101.60 distinct_points( Z, intersection_point( X, Y ) ), ! apart_point_and_line
% 101.23/101.60 ( Z, Y ) }.
% 101.23/101.60 parent0: (11801) {G0,W11,D3,L3,V3,M3} { ! convergent_lines( X, Y ), !
% 101.23/101.60 apart_point_and_line( Z, Y ), distinct_points( Z, intersection_point( X,
% 101.23/101.60 Y ) ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := X
% 101.23/101.60 Y := Y
% 101.23/101.60 Z := Z
% 101.23/101.60 end
% 101.23/101.60 permutation0:
% 101.23/101.60 0 ==> 0
% 101.23/101.60 1 ==> 2
% 101.23/101.60 2 ==> 1
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 subsumption: (11) {G0,W9,D2,L3,V3,M2} I { distinct_points( X, Z ),
% 101.23/101.60 apart_point_and_line( Z, Y ), ! apart_point_and_line( X, Y ) }.
% 101.23/101.60 parent0: (11803) {G0,W9,D2,L3,V3,M3} { ! apart_point_and_line( X, Y ),
% 101.23/101.60 distinct_points( X, Z ), apart_point_and_line( Z, Y ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := X
% 101.23/101.60 Y := Y
% 101.23/101.60 Z := Z
% 101.23/101.60 end
% 101.23/101.60 permutation0:
% 101.23/101.60 0 ==> 2
% 101.23/101.60 1 ==> 0
% 101.23/101.60 2 ==> 1
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 subsumption: (12) {G0,W9,D2,L3,V3,M2} I { distinct_lines( Y, Z ),
% 101.23/101.60 apart_point_and_line( X, Z ), ! apart_point_and_line( X, Y ) }.
% 101.23/101.60 parent0: (11804) {G0,W9,D2,L3,V3,M3} { ! apart_point_and_line( X, Y ),
% 101.23/101.60 distinct_lines( Y, Z ), apart_point_and_line( X, Z ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := X
% 101.23/101.60 Y := Y
% 101.23/101.60 Z := Z
% 101.23/101.60 end
% 101.23/101.60 permutation0:
% 101.23/101.60 0 ==> 2
% 101.23/101.60 1 ==> 0
% 101.23/101.60 2 ==> 1
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 subsumption: (13) {G0,W6,D2,L2,V2,M1} I { ! convergent_lines( X, Y ),
% 101.23/101.60 distinct_lines( X, Y ) }.
% 101.23/101.60 parent0: (11805) {G0,W6,D2,L2,V2,M2} { ! convergent_lines( X, Y ),
% 101.23/101.60 distinct_lines( X, Y ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := X
% 101.23/101.60 Y := Y
% 101.23/101.60 end
% 101.23/101.60 permutation0:
% 101.23/101.60 0 ==> 0
% 101.23/101.60 1 ==> 1
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 subsumption: (14) {G0,W5,D3,L1,V2,M1} I { ! convergent_lines(
% 101.23/101.60 parallel_through_point( Y, X ), Y ) }.
% 101.23/101.60 parent0: (11806) {G0,W5,D3,L1,V2,M1} { ! convergent_lines(
% 101.23/101.60 parallel_through_point( Y, X ), Y ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := X
% 101.23/101.60 Y := Y
% 101.23/101.60 end
% 101.23/101.60 permutation0:
% 101.23/101.60 0 ==> 0
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 subsumption: (15) {G0,W5,D3,L1,V2,M1} I { ! apart_point_and_line( X,
% 101.23/101.60 parallel_through_point( Y, X ) ) }.
% 101.23/101.60 parent0: (11807) {G0,W5,D3,L1,V2,M1} { ! apart_point_and_line( X,
% 101.23/101.60 parallel_through_point( Y, X ) ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := X
% 101.23/101.60 Y := Y
% 101.23/101.60 end
% 101.23/101.60 permutation0:
% 101.23/101.60 0 ==> 0
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 subsumption: (16) {G0,W12,D2,L4,V3,M2} I { ! distinct_lines( X, Y ),
% 101.23/101.60 convergent_lines( X, Y ), apart_point_and_line( Z, X ),
% 101.23/101.60 apart_point_and_line( Z, Y ) }.
% 101.23/101.60 parent0: (11808) {G0,W12,D2,L4,V3,M4} { ! distinct_lines( X, Y ),
% 101.23/101.60 apart_point_and_line( Z, X ), apart_point_and_line( Z, Y ),
% 101.23/101.60 convergent_lines( X, Y ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := X
% 101.23/101.60 Y := Y
% 101.23/101.60 Z := Z
% 101.23/101.60 end
% 101.23/101.60 permutation0:
% 101.23/101.60 0 ==> 0
% 101.23/101.60 1 ==> 2
% 101.23/101.60 2 ==> 3
% 101.23/101.60 3 ==> 1
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 subsumption: (17) {G0,W6,D2,L2,V2,M1} I { convergent_lines( X, Y ),
% 101.23/101.60 unorthogonal_lines( X, Y ) }.
% 101.23/101.60 parent0: (11809) {G0,W6,D2,L2,V2,M2} { convergent_lines( X, Y ),
% 101.23/101.60 unorthogonal_lines( X, Y ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := X
% 101.23/101.60 Y := Y
% 101.23/101.60 end
% 101.23/101.60 permutation0:
% 101.23/101.60 0 ==> 0
% 101.23/101.60 1 ==> 1
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 subsumption: (18) {G0,W12,D2,L4,V3,M1} I { ! convergent_lines( X, Y ), !
% 101.23/101.60 unorthogonal_lines( X, Y ), convergent_lines( Y, Z ), alpha1( X, Z ) }.
% 101.23/101.60 parent0: (11810) {G0,W12,D2,L4,V3,M4} { ! convergent_lines( X, Y ), !
% 101.23/101.60 unorthogonal_lines( X, Y ), alpha1( X, Z ), convergent_lines( Y, Z ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := X
% 101.23/101.60 Y := Y
% 101.23/101.60 Z := Z
% 101.23/101.60 end
% 101.23/101.60 permutation0:
% 101.23/101.60 0 ==> 0
% 101.23/101.60 1 ==> 1
% 101.23/101.60 2 ==> 3
% 101.23/101.60 3 ==> 2
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 subsumption: (19) {G0,W12,D2,L4,V3,M1} I { ! convergent_lines( X, Y ), !
% 101.23/101.60 unorthogonal_lines( X, Y ), unorthogonal_lines( Y, Z ), alpha1( X, Z )
% 101.23/101.60 }.
% 101.23/101.60 parent0: (11811) {G0,W12,D2,L4,V3,M4} { ! convergent_lines( X, Y ), !
% 101.23/101.60 unorthogonal_lines( X, Y ), alpha1( X, Z ), unorthogonal_lines( Y, Z )
% 101.23/101.60 }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := X
% 101.23/101.60 Y := Y
% 101.23/101.60 Z := Z
% 101.23/101.60 end
% 101.23/101.60 permutation0:
% 101.23/101.60 0 ==> 0
% 101.23/101.60 1 ==> 1
% 101.23/101.60 2 ==> 3
% 101.23/101.60 3 ==> 2
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 subsumption: (20) {G0,W6,D2,L2,V2,M1} I { convergent_lines( X, Y ), !
% 101.23/101.60 alpha1( X, Y ) }.
% 101.23/101.60 parent0: (11812) {G0,W6,D2,L2,V2,M2} { ! alpha1( X, Y ), convergent_lines
% 101.23/101.60 ( X, Y ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := X
% 101.23/101.60 Y := Y
% 101.23/101.60 end
% 101.23/101.60 permutation0:
% 101.23/101.60 0 ==> 1
% 101.23/101.60 1 ==> 0
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 subsumption: (21) {G0,W6,D2,L2,V2,M1} I { unorthogonal_lines( X, Y ), !
% 101.23/101.60 alpha1( X, Y ) }.
% 101.23/101.60 parent0: (11813) {G0,W6,D2,L2,V2,M2} { ! alpha1( X, Y ),
% 101.23/101.60 unorthogonal_lines( X, Y ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := X
% 101.23/101.60 Y := Y
% 101.23/101.60 end
% 101.23/101.60 permutation0:
% 101.23/101.60 0 ==> 1
% 101.23/101.60 1 ==> 0
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 subsumption: (23) {G0,W5,D3,L1,V2,M1} I { ! unorthogonal_lines(
% 101.23/101.60 orthogonal_through_point( Y, X ), Y ) }.
% 101.23/101.60 parent0: (11815) {G0,W5,D3,L1,V2,M1} { ! unorthogonal_lines(
% 101.23/101.60 orthogonal_through_point( Y, X ), Y ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := X
% 101.23/101.60 Y := Y
% 101.23/101.60 end
% 101.23/101.60 permutation0:
% 101.23/101.60 0 ==> 0
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 subsumption: (24) {G0,W5,D3,L1,V2,M1} I { ! apart_point_and_line( X,
% 101.23/101.60 orthogonal_through_point( Y, X ) ) }.
% 101.23/101.60 parent0: (11816) {G0,W5,D3,L1,V2,M1} { ! apart_point_and_line( X,
% 101.23/101.60 orthogonal_through_point( Y, X ) ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := X
% 101.23/101.60 Y := Y
% 101.23/101.60 end
% 101.23/101.60 permutation0:
% 101.23/101.60 0 ==> 0
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 subsumption: (25) {G0,W15,D2,L5,V4,M2} I { ! distinct_lines( X, Y ),
% 101.23/101.60 apart_point_and_line( Z, X ), apart_point_and_line( Z, Y ),
% 101.23/101.60 unorthogonal_lines( Y, T ), unorthogonal_lines( X, T ) }.
% 101.23/101.60 parent0: (11817) {G0,W15,D2,L5,V4,M5} { ! distinct_lines( X, Y ),
% 101.23/101.60 apart_point_and_line( Z, X ), apart_point_and_line( Z, Y ),
% 101.23/101.60 unorthogonal_lines( X, T ), unorthogonal_lines( Y, T ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := X
% 101.23/101.60 Y := Y
% 101.23/101.60 Z := Z
% 101.23/101.60 T := T
% 101.23/101.60 end
% 101.23/101.60 permutation0:
% 101.23/101.60 0 ==> 0
% 101.23/101.60 1 ==> 1
% 101.23/101.60 2 ==> 2
% 101.23/101.60 3 ==> 4
% 101.23/101.60 4 ==> 3
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 subsumption: (26) {G0,W9,D4,L1,V0,M1} I { distinct_lines(
% 101.23/101.60 parallel_through_point( skol2, skol1 ), orthogonal_through_point(
% 101.23/101.60 orthogonal_through_point( skol2, skol1 ), skol1 ) ) }.
% 101.23/101.60 parent0: (11818) {G0,W9,D4,L1,V0,M1} { distinct_lines(
% 101.23/101.60 parallel_through_point( skol2, skol1 ), orthogonal_through_point(
% 101.23/101.60 orthogonal_through_point( skol2, skol1 ), skol1 ) ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 end
% 101.23/101.60 permutation0:
% 101.23/101.60 0 ==> 0
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 resolution: (11979) {G1,W6,D2,L2,V2,M2} { distinct_lines( Y, X ), !
% 101.23/101.60 distinct_lines( X, Y ) }.
% 101.23/101.60 parent0[0]: (1) {G0,W3,D2,L1,V1,M1} I { ! distinct_lines( X, X ) }.
% 101.23/101.60 parent1[0]: (4) {G0,W9,D2,L3,V3,M3} I { distinct_lines( X, Z ),
% 101.23/101.60 distinct_lines( Y, Z ), ! distinct_lines( X, Y ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := X
% 101.23/101.60 end
% 101.23/101.60 substitution1:
% 101.23/101.60 X := X
% 101.23/101.60 Y := Y
% 101.23/101.60 Z := X
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 subsumption: (34) {G1,W6,D2,L2,V2,M2} R(4,1) { ! distinct_lines( Y, X ),
% 101.23/101.60 distinct_lines( X, Y ) }.
% 101.23/101.60 parent0: (11979) {G1,W6,D2,L2,V2,M2} { distinct_lines( Y, X ), !
% 101.23/101.60 distinct_lines( X, Y ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := Y
% 101.23/101.60 Y := X
% 101.23/101.60 end
% 101.23/101.60 permutation0:
% 101.23/101.60 0 ==> 1
% 101.23/101.60 1 ==> 0
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 resolution: (11981) {G1,W5,D3,L1,V2,M1} { convergent_lines(
% 101.23/101.60 orthogonal_through_point( X, Y ), X ) }.
% 101.23/101.60 parent0[0]: (23) {G0,W5,D3,L1,V2,M1} I { ! unorthogonal_lines(
% 101.23/101.60 orthogonal_through_point( Y, X ), Y ) }.
% 101.23/101.60 parent1[1]: (17) {G0,W6,D2,L2,V2,M1} I { convergent_lines( X, Y ),
% 101.23/101.60 unorthogonal_lines( X, Y ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := Y
% 101.23/101.60 Y := X
% 101.23/101.60 end
% 101.23/101.60 substitution1:
% 101.23/101.60 X := orthogonal_through_point( X, Y )
% 101.23/101.60 Y := X
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 subsumption: (37) {G1,W5,D3,L1,V2,M1} R(17,23) { convergent_lines(
% 101.23/101.60 orthogonal_through_point( X, Y ), X ) }.
% 101.23/101.60 parent0: (11981) {G1,W5,D3,L1,V2,M1} { convergent_lines(
% 101.23/101.60 orthogonal_through_point( X, Y ), X ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := X
% 101.23/101.60 Y := Y
% 101.23/101.60 end
% 101.23/101.60 permutation0:
% 101.23/101.60 0 ==> 0
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 resolution: (11982) {G1,W8,D3,L2,V3,M2} { convergent_lines(
% 101.23/101.60 orthogonal_through_point( X, Y ), Z ), convergent_lines( X, Z ) }.
% 101.23/101.60 parent0[2]: (5) {G0,W9,D2,L3,V3,M3} I { convergent_lines( X, Z ),
% 101.23/101.60 convergent_lines( Y, Z ), ! convergent_lines( X, Y ) }.
% 101.23/101.60 parent1[0]: (37) {G1,W5,D3,L1,V2,M1} R(17,23) { convergent_lines(
% 101.23/101.60 orthogonal_through_point( X, Y ), X ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := orthogonal_through_point( X, Y )
% 101.23/101.60 Y := X
% 101.23/101.60 Z := Z
% 101.23/101.60 end
% 101.23/101.60 substitution1:
% 101.23/101.60 X := X
% 101.23/101.60 Y := Y
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 subsumption: (40) {G2,W8,D3,L2,V3,M2} R(5,37) { convergent_lines( X, Z ),
% 101.23/101.60 convergent_lines( orthogonal_through_point( X, Y ), Z ) }.
% 101.23/101.60 parent0: (11982) {G1,W8,D3,L2,V3,M2} { convergent_lines(
% 101.23/101.60 orthogonal_through_point( X, Y ), Z ), convergent_lines( X, Z ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := X
% 101.23/101.60 Y := Y
% 101.23/101.60 Z := Z
% 101.23/101.60 end
% 101.23/101.60 permutation0:
% 101.23/101.60 0 ==> 1
% 101.23/101.60 1 ==> 0
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 resolution: (11983) {G1,W8,D3,L2,V3,M2} { convergent_lines( Z, X ), !
% 101.23/101.60 convergent_lines( parallel_through_point( X, Y ), Z ) }.
% 101.23/101.60 parent0[0]: (14) {G0,W5,D3,L1,V2,M1} I { ! convergent_lines(
% 101.23/101.60 parallel_through_point( Y, X ), Y ) }.
% 101.23/101.60 parent1[0]: (5) {G0,W9,D2,L3,V3,M3} I { convergent_lines( X, Z ),
% 101.23/101.60 convergent_lines( Y, Z ), ! convergent_lines( X, Y ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := Y
% 101.23/101.60 Y := X
% 101.23/101.60 end
% 101.23/101.60 substitution1:
% 101.23/101.60 X := parallel_through_point( X, Y )
% 101.23/101.60 Y := Z
% 101.23/101.60 Z := X
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 subsumption: (41) {G1,W8,D3,L2,V3,M2} R(5,14) { ! convergent_lines(
% 101.23/101.60 parallel_through_point( Y, Z ), X ), convergent_lines( X, Y ) }.
% 101.23/101.60 parent0: (11983) {G1,W8,D3,L2,V3,M2} { convergent_lines( Z, X ), !
% 101.23/101.60 convergent_lines( parallel_through_point( X, Y ), Z ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := Y
% 101.23/101.60 Y := Z
% 101.23/101.60 Z := X
% 101.23/101.60 end
% 101.23/101.60 permutation0:
% 101.23/101.60 0 ==> 1
% 101.23/101.60 1 ==> 0
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 resolution: (11985) {G1,W6,D2,L2,V2,M2} { convergent_lines( Y, X ), !
% 101.23/101.60 convergent_lines( X, Y ) }.
% 101.23/101.60 parent0[0]: (2) {G0,W3,D2,L1,V1,M1} I { ! convergent_lines( X, X ) }.
% 101.23/101.60 parent1[0]: (5) {G0,W9,D2,L3,V3,M3} I { convergent_lines( X, Z ),
% 101.23/101.60 convergent_lines( Y, Z ), ! convergent_lines( X, Y ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := X
% 101.23/101.60 end
% 101.23/101.60 substitution1:
% 101.23/101.60 X := X
% 101.23/101.60 Y := Y
% 101.23/101.60 Z := X
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 subsumption: (43) {G1,W6,D2,L2,V2,M2} R(5,2) { ! convergent_lines( Y, X ),
% 101.23/101.60 convergent_lines( X, Y ) }.
% 101.23/101.60 parent0: (11985) {G1,W6,D2,L2,V2,M2} { convergent_lines( Y, X ), !
% 101.23/101.60 convergent_lines( X, Y ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := Y
% 101.23/101.60 Y := X
% 101.23/101.60 end
% 101.23/101.60 permutation0:
% 101.23/101.60 0 ==> 1
% 101.23/101.60 1 ==> 0
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 resolution: (11988) {G1,W9,D2,L3,V3,M3} { convergent_lines( Y, X ),
% 101.23/101.60 convergent_lines( Z, Y ), ! convergent_lines( Z, X ) }.
% 101.23/101.60 parent0[0]: (43) {G1,W6,D2,L2,V2,M2} R(5,2) { ! convergent_lines( Y, X ),
% 101.23/101.60 convergent_lines( X, Y ) }.
% 101.23/101.60 parent1[1]: (5) {G0,W9,D2,L3,V3,M3} I { convergent_lines( X, Z ),
% 101.23/101.60 convergent_lines( Y, Z ), ! convergent_lines( X, Y ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := Y
% 101.23/101.60 Y := X
% 101.23/101.60 end
% 101.23/101.60 substitution1:
% 101.23/101.60 X := Z
% 101.23/101.60 Y := X
% 101.23/101.60 Z := Y
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 subsumption: (45) {G2,W9,D2,L3,V3,M3} R(43,5) { convergent_lines( Z, X ), !
% 101.23/101.60 convergent_lines( Z, Y ), convergent_lines( X, Y ) }.
% 101.23/101.60 parent0: (11988) {G1,W9,D2,L3,V3,M3} { convergent_lines( Y, X ),
% 101.23/101.60 convergent_lines( Z, Y ), ! convergent_lines( Z, X ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := Y
% 101.23/101.60 Y := X
% 101.23/101.60 Z := Z
% 101.23/101.60 end
% 101.23/101.60 permutation0:
% 101.23/101.60 0 ==> 2
% 101.23/101.60 1 ==> 0
% 101.23/101.60 2 ==> 1
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 resolution: (11990) {G2,W5,D3,L1,V2,M1} { convergent_lines( X,
% 101.23/101.60 orthogonal_through_point( X, Y ) ) }.
% 101.23/101.60 parent0[0]: (43) {G1,W6,D2,L2,V2,M2} R(5,2) { ! convergent_lines( Y, X ),
% 101.23/101.60 convergent_lines( X, Y ) }.
% 101.23/101.60 parent1[0]: (37) {G1,W5,D3,L1,V2,M1} R(17,23) { convergent_lines(
% 101.23/101.60 orthogonal_through_point( X, Y ), X ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := X
% 101.23/101.60 Y := orthogonal_through_point( X, Y )
% 101.23/101.60 end
% 101.23/101.60 substitution1:
% 101.23/101.60 X := X
% 101.23/101.60 Y := Y
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 subsumption: (46) {G2,W5,D3,L1,V2,M1} R(43,37) { convergent_lines( X,
% 101.23/101.60 orthogonal_through_point( X, Y ) ) }.
% 101.23/101.60 parent0: (11990) {G2,W5,D3,L1,V2,M1} { convergent_lines( X,
% 101.23/101.60 orthogonal_through_point( X, Y ) ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := X
% 101.23/101.60 Y := Y
% 101.23/101.60 end
% 101.23/101.60 permutation0:
% 101.23/101.60 0 ==> 0
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 resolution: (11991) {G2,W8,D3,L2,V3,M2} { convergent_lines( Y, X ),
% 101.23/101.60 convergent_lines( orthogonal_through_point( X, Z ), Y ) }.
% 101.23/101.60 parent0[0]: (43) {G1,W6,D2,L2,V2,M2} R(5,2) { ! convergent_lines( Y, X ),
% 101.23/101.60 convergent_lines( X, Y ) }.
% 101.23/101.60 parent1[0]: (40) {G2,W8,D3,L2,V3,M2} R(5,37) { convergent_lines( X, Z ),
% 101.23/101.60 convergent_lines( orthogonal_through_point( X, Y ), Z ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := Y
% 101.23/101.60 Y := X
% 101.23/101.60 end
% 101.23/101.60 substitution1:
% 101.23/101.60 X := X
% 101.23/101.60 Y := Z
% 101.23/101.60 Z := Y
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 subsumption: (93) {G3,W8,D3,L2,V3,M2} R(40,43) { convergent_lines( Z, X ),
% 101.23/101.60 convergent_lines( orthogonal_through_point( X, Y ), Z ) }.
% 101.23/101.60 parent0: (11991) {G2,W8,D3,L2,V3,M2} { convergent_lines( Y, X ),
% 101.23/101.60 convergent_lines( orthogonal_through_point( X, Z ), Y ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := X
% 101.23/101.60 Y := Z
% 101.23/101.60 Z := Y
% 101.23/101.60 end
% 101.23/101.60 permutation0:
% 101.23/101.60 0 ==> 0
% 101.23/101.60 1 ==> 1
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 resolution: (11994) {G1,W11,D3,L3,V4,M3} { convergent_lines( Z, X ),
% 101.23/101.60 convergent_lines( T, Z ), ! convergent_lines( T, parallel_through_point(
% 101.23/101.60 X, Y ) ) }.
% 101.23/101.60 parent0[0]: (41) {G1,W8,D3,L2,V3,M2} R(5,14) { ! convergent_lines(
% 101.23/101.60 parallel_through_point( Y, Z ), X ), convergent_lines( X, Y ) }.
% 101.23/101.60 parent1[1]: (5) {G0,W9,D2,L3,V3,M3} I { convergent_lines( X, Z ),
% 101.23/101.60 convergent_lines( Y, Z ), ! convergent_lines( X, Y ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := Z
% 101.23/101.60 Y := X
% 101.23/101.60 Z := Y
% 101.23/101.60 end
% 101.23/101.60 substitution1:
% 101.23/101.60 X := T
% 101.23/101.60 Y := parallel_through_point( X, Y )
% 101.23/101.60 Z := Z
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 subsumption: (151) {G2,W11,D3,L3,V4,M3} R(41,5) { convergent_lines( Z, X )
% 101.23/101.60 , ! convergent_lines( Z, parallel_through_point( Y, T ) ),
% 101.23/101.60 convergent_lines( X, Y ) }.
% 101.23/101.60 parent0: (11994) {G1,W11,D3,L3,V4,M3} { convergent_lines( Z, X ),
% 101.23/101.60 convergent_lines( T, Z ), ! convergent_lines( T, parallel_through_point(
% 101.23/101.60 X, Y ) ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := Y
% 101.23/101.60 Y := T
% 101.23/101.60 Z := X
% 101.23/101.60 T := Z
% 101.23/101.60 end
% 101.23/101.60 permutation0:
% 101.23/101.60 0 ==> 2
% 101.23/101.60 1 ==> 0
% 101.23/101.60 2 ==> 1
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 resolution: (11997) {G1,W14,D3,L4,V4,M4} { ! convergent_lines( X, Y ),
% 101.23/101.60 distinct_points( Z, intersection_point( X, Y ) ), distinct_points( T, Z )
% 101.23/101.60 , ! apart_point_and_line( T, Y ) }.
% 101.23/101.60 parent0[2]: (9) {G0,W11,D3,L3,V3,M1} I { ! convergent_lines( X, Y ),
% 101.23/101.60 distinct_points( Z, intersection_point( X, Y ) ), ! apart_point_and_line
% 101.23/101.60 ( Z, Y ) }.
% 101.23/101.60 parent1[1]: (11) {G0,W9,D2,L3,V3,M2} I { distinct_points( X, Z ),
% 101.23/101.60 apart_point_and_line( Z, Y ), ! apart_point_and_line( X, Y ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := X
% 101.23/101.60 Y := Y
% 101.23/101.60 Z := Z
% 101.23/101.60 end
% 101.23/101.60 substitution1:
% 101.23/101.60 X := T
% 101.23/101.60 Y := Y
% 101.23/101.60 Z := Z
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 subsumption: (167) {G1,W14,D3,L4,V4,M1} R(11,9) { distinct_points( X, Y ),
% 101.23/101.60 ! convergent_lines( T, Z ), distinct_points( Y, intersection_point( T, Z
% 101.23/101.60 ) ), ! apart_point_and_line( X, Z ) }.
% 101.23/101.60 parent0: (11997) {G1,W14,D3,L4,V4,M4} { ! convergent_lines( X, Y ),
% 101.23/101.60 distinct_points( Z, intersection_point( X, Y ) ), distinct_points( T, Z )
% 101.23/101.60 , ! apart_point_and_line( T, Y ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := T
% 101.23/101.60 Y := Z
% 101.23/101.60 Z := Y
% 101.23/101.60 T := X
% 101.23/101.60 end
% 101.23/101.60 permutation0:
% 101.23/101.60 0 ==> 1
% 101.23/101.60 1 ==> 2
% 101.23/101.60 2 ==> 0
% 101.23/101.60 3 ==> 3
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 resolution: (11999) {G1,W14,D3,L4,V4,M4} { ! convergent_lines( X, Y ),
% 101.23/101.60 distinct_points( Z, intersection_point( X, Y ) ), distinct_points( T, Z )
% 101.23/101.60 , ! apart_point_and_line( T, X ) }.
% 101.23/101.60 parent0[2]: (8) {G0,W11,D3,L3,V3,M1} I { ! convergent_lines( X, Y ),
% 101.23/101.60 distinct_points( Z, intersection_point( X, Y ) ), ! apart_point_and_line
% 101.23/101.60 ( Z, X ) }.
% 101.23/101.60 parent1[1]: (11) {G0,W9,D2,L3,V3,M2} I { distinct_points( X, Z ),
% 101.23/101.60 apart_point_and_line( Z, Y ), ! apart_point_and_line( X, Y ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := X
% 101.23/101.60 Y := Y
% 101.23/101.60 Z := Z
% 101.23/101.60 end
% 101.23/101.60 substitution1:
% 101.23/101.60 X := T
% 101.23/101.60 Y := X
% 101.23/101.60 Z := Z
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 subsumption: (168) {G1,W14,D3,L4,V4,M1} R(11,8) { distinct_points( X, Y ),
% 101.23/101.60 ! convergent_lines( Z, T ), distinct_points( Y, intersection_point( Z, T
% 101.23/101.60 ) ), ! apart_point_and_line( X, Z ) }.
% 101.23/101.60 parent0: (11999) {G1,W14,D3,L4,V4,M4} { ! convergent_lines( X, Y ),
% 101.23/101.60 distinct_points( Z, intersection_point( X, Y ) ), distinct_points( T, Z )
% 101.23/101.60 , ! apart_point_and_line( T, X ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := Z
% 101.23/101.60 Y := T
% 101.23/101.60 Z := Y
% 101.23/101.60 T := X
% 101.23/101.60 end
% 101.23/101.60 permutation0:
% 101.23/101.60 0 ==> 1
% 101.23/101.60 1 ==> 2
% 101.23/101.60 2 ==> 0
% 101.23/101.60 3 ==> 3
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 factor: (12001) {G1,W15,D3,L3,V2,M3} { distinct_points( intersection_point
% 101.23/101.60 ( X, Y ), intersection_point( X, Y ) ), ! convergent_lines( X, Y ), !
% 101.23/101.60 apart_point_and_line( intersection_point( X, Y ), X ) }.
% 101.23/101.60 parent0[0, 2]: (168) {G1,W14,D3,L4,V4,M1} R(11,8) { distinct_points( X, Y )
% 101.23/101.60 , ! convergent_lines( Z, T ), distinct_points( Y, intersection_point( Z,
% 101.23/101.60 T ) ), ! apart_point_and_line( X, Z ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := intersection_point( X, Y )
% 101.23/101.60 Y := intersection_point( X, Y )
% 101.23/101.60 Z := X
% 101.23/101.60 T := Y
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 resolution: (12002) {G1,W8,D3,L2,V2,M2} { ! convergent_lines( X, Y ), !
% 101.23/101.60 apart_point_and_line( intersection_point( X, Y ), X ) }.
% 101.23/101.60 parent0[0]: (0) {G0,W3,D2,L1,V1,M1} I { ! distinct_points( X, X ) }.
% 101.23/101.60 parent1[0]: (12001) {G1,W15,D3,L3,V2,M3} { distinct_points(
% 101.23/101.60 intersection_point( X, Y ), intersection_point( X, Y ) ), !
% 101.23/101.60 convergent_lines( X, Y ), ! apart_point_and_line( intersection_point( X,
% 101.23/101.60 Y ), X ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := intersection_point( X, Y )
% 101.23/101.60 end
% 101.23/101.60 substitution1:
% 101.23/101.60 X := X
% 101.23/101.60 Y := Y
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 subsumption: (175) {G2,W8,D3,L2,V2,M1} F(168);r(0) { ! convergent_lines( X
% 101.23/101.60 , Y ), ! apart_point_and_line( intersection_point( X, Y ), X ) }.
% 101.23/101.60 parent0: (12002) {G1,W8,D3,L2,V2,M2} { ! convergent_lines( X, Y ), !
% 101.23/101.60 apart_point_and_line( intersection_point( X, Y ), X ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := X
% 101.23/101.60 Y := Y
% 101.23/101.60 end
% 101.23/101.60 permutation0:
% 101.23/101.60 0 ==> 0
% 101.23/101.60 1 ==> 1
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 factor: (12003) {G1,W15,D3,L3,V2,M3} { distinct_points( intersection_point
% 101.23/101.60 ( X, Y ), intersection_point( X, Y ) ), ! convergent_lines( X, Y ), !
% 101.23/101.60 apart_point_and_line( intersection_point( X, Y ), Y ) }.
% 101.23/101.60 parent0[0, 2]: (167) {G1,W14,D3,L4,V4,M1} R(11,9) { distinct_points( X, Y )
% 101.23/101.60 , ! convergent_lines( T, Z ), distinct_points( Y, intersection_point( T,
% 101.23/101.60 Z ) ), ! apart_point_and_line( X, Z ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := intersection_point( X, Y )
% 101.23/101.60 Y := intersection_point( X, Y )
% 101.23/101.60 Z := Y
% 101.23/101.60 T := X
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 resolution: (12004) {G1,W8,D3,L2,V2,M2} { ! convergent_lines( X, Y ), !
% 101.23/101.60 apart_point_and_line( intersection_point( X, Y ), Y ) }.
% 101.23/101.60 parent0[0]: (0) {G0,W3,D2,L1,V1,M1} I { ! distinct_points( X, X ) }.
% 101.23/101.60 parent1[0]: (12003) {G1,W15,D3,L3,V2,M3} { distinct_points(
% 101.23/101.60 intersection_point( X, Y ), intersection_point( X, Y ) ), !
% 101.23/101.60 convergent_lines( X, Y ), ! apart_point_and_line( intersection_point( X,
% 101.23/101.60 Y ), Y ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := intersection_point( X, Y )
% 101.23/101.60 end
% 101.23/101.60 substitution1:
% 101.23/101.60 X := X
% 101.23/101.60 Y := Y
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 subsumption: (176) {G2,W8,D3,L2,V2,M1} F(167);r(0) { ! convergent_lines( X
% 101.23/101.60 , Y ), ! apart_point_and_line( intersection_point( X, Y ), Y ) }.
% 101.23/101.60 parent0: (12004) {G1,W8,D3,L2,V2,M2} { ! convergent_lines( X, Y ), !
% 101.23/101.60 apart_point_and_line( intersection_point( X, Y ), Y ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := X
% 101.23/101.60 Y := Y
% 101.23/101.60 end
% 101.23/101.60 permutation0:
% 101.23/101.60 0 ==> 0
% 101.23/101.60 1 ==> 1
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 resolution: (12005) {G1,W8,D3,L2,V3,M2} { distinct_lines( Z,
% 101.23/101.60 orthogonal_through_point( Y, X ) ), ! apart_point_and_line( X, Z ) }.
% 101.23/101.60 parent0[0]: (24) {G0,W5,D3,L1,V2,M1} I { ! apart_point_and_line( X,
% 101.23/101.60 orthogonal_through_point( Y, X ) ) }.
% 101.23/101.60 parent1[1]: (12) {G0,W9,D2,L3,V3,M2} I { distinct_lines( Y, Z ),
% 101.23/101.60 apart_point_and_line( X, Z ), ! apart_point_and_line( X, Y ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := X
% 101.23/101.60 Y := Y
% 101.23/101.60 end
% 101.23/101.60 substitution1:
% 101.23/101.60 X := X
% 101.23/101.60 Y := Z
% 101.23/101.60 Z := orthogonal_through_point( Y, X )
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 subsumption: (196) {G1,W8,D3,L2,V3,M1} R(12,24) { distinct_lines( X,
% 101.23/101.60 orthogonal_through_point( Y, Z ) ), ! apart_point_and_line( Z, X ) }.
% 101.23/101.60 parent0: (12005) {G1,W8,D3,L2,V3,M2} { distinct_lines( Z,
% 101.23/101.60 orthogonal_through_point( Y, X ) ), ! apart_point_and_line( X, Z ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := Z
% 101.23/101.60 Y := Y
% 101.23/101.60 Z := X
% 101.23/101.60 end
% 101.23/101.60 permutation0:
% 101.23/101.60 0 ==> 0
% 101.23/101.60 1 ==> 1
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 resolution: (12006) {G1,W11,D3,L3,V4,M3} { distinct_lines( X,
% 101.23/101.60 orthogonal_through_point( Y, Z ) ), distinct_lines( T, X ), !
% 101.23/101.60 apart_point_and_line( Z, T ) }.
% 101.23/101.60 parent0[1]: (196) {G1,W8,D3,L2,V3,M1} R(12,24) { distinct_lines( X,
% 101.23/101.60 orthogonal_through_point( Y, Z ) ), ! apart_point_and_line( Z, X ) }.
% 101.23/101.60 parent1[1]: (12) {G0,W9,D2,L3,V3,M2} I { distinct_lines( Y, Z ),
% 101.23/101.60 apart_point_and_line( X, Z ), ! apart_point_and_line( X, Y ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := X
% 101.23/101.60 Y := Y
% 101.23/101.60 Z := Z
% 101.23/101.60 end
% 101.23/101.60 substitution1:
% 101.23/101.60 X := Z
% 101.23/101.60 Y := T
% 101.23/101.60 Z := X
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 subsumption: (198) {G2,W11,D3,L3,V4,M1} R(196,12) { distinct_lines( X,
% 101.23/101.60 orthogonal_through_point( Y, Z ) ), distinct_lines( T, X ), !
% 101.23/101.60 apart_point_and_line( Z, T ) }.
% 101.23/101.60 parent0: (12006) {G1,W11,D3,L3,V4,M3} { distinct_lines( X,
% 101.23/101.60 orthogonal_through_point( Y, Z ) ), distinct_lines( T, X ), !
% 101.23/101.60 apart_point_and_line( Z, T ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := X
% 101.23/101.60 Y := Y
% 101.23/101.60 Z := Z
% 101.23/101.60 T := T
% 101.23/101.60 end
% 101.23/101.60 permutation0:
% 101.23/101.60 0 ==> 0
% 101.23/101.60 1 ==> 1
% 101.23/101.60 2 ==> 2
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 resolution: (12009) {G1,W13,D3,L3,V3,M3} { ! distinct_lines( Z,
% 101.23/101.60 parallel_through_point( Y, X ) ), convergent_lines( Z,
% 101.23/101.60 parallel_through_point( Y, X ) ), apart_point_and_line( X, Z ) }.
% 101.23/101.60 parent0[0]: (15) {G0,W5,D3,L1,V2,M1} I { ! apart_point_and_line( X,
% 101.23/101.60 parallel_through_point( Y, X ) ) }.
% 101.23/101.60 parent1[3]: (16) {G0,W12,D2,L4,V3,M2} I { ! distinct_lines( X, Y ),
% 101.23/101.60 convergent_lines( X, Y ), apart_point_and_line( Z, X ),
% 101.23/101.60 apart_point_and_line( Z, Y ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := X
% 101.23/101.60 Y := Y
% 101.23/101.60 end
% 101.23/101.60 substitution1:
% 101.23/101.60 X := Z
% 101.23/101.60 Y := parallel_through_point( Y, X )
% 101.23/101.60 Z := X
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 subsumption: (226) {G1,W13,D3,L3,V3,M1} R(16,15) { convergent_lines( X,
% 101.23/101.60 parallel_through_point( Y, Z ) ), ! distinct_lines( X,
% 101.23/101.60 parallel_through_point( Y, Z ) ), apart_point_and_line( Z, X ) }.
% 101.23/101.60 parent0: (12009) {G1,W13,D3,L3,V3,M3} { ! distinct_lines( Z,
% 101.23/101.60 parallel_through_point( Y, X ) ), convergent_lines( Z,
% 101.23/101.60 parallel_through_point( Y, X ) ), apart_point_and_line( X, Z ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := Z
% 101.23/101.60 Y := Y
% 101.23/101.60 Z := X
% 101.23/101.60 end
% 101.23/101.60 permutation0:
% 101.23/101.60 0 ==> 1
% 101.23/101.60 1 ==> 0
% 101.23/101.60 2 ==> 2
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 resolution: (12011) {G1,W12,D2,L4,V3,M4} { unorthogonal_lines( X, Y ), !
% 101.23/101.60 convergent_lines( X, Z ), ! unorthogonal_lines( X, Z ), convergent_lines
% 101.23/101.60 ( Z, Y ) }.
% 101.23/101.60 parent0[1]: (21) {G0,W6,D2,L2,V2,M1} I { unorthogonal_lines( X, Y ), !
% 101.23/101.60 alpha1( X, Y ) }.
% 101.23/101.60 parent1[3]: (18) {G0,W12,D2,L4,V3,M1} I { ! convergent_lines( X, Y ), !
% 101.23/101.60 unorthogonal_lines( X, Y ), convergent_lines( Y, Z ), alpha1( X, Z ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := X
% 101.23/101.60 Y := Y
% 101.23/101.60 end
% 101.23/101.60 substitution1:
% 101.23/101.60 X := X
% 101.23/101.60 Y := Z
% 101.23/101.60 Z := Y
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 subsumption: (241) {G1,W12,D2,L4,V3,M2} R(18,21) { ! convergent_lines( X, Y
% 101.23/101.60 ), convergent_lines( Y, Z ), unorthogonal_lines( X, Z ), !
% 101.23/101.60 unorthogonal_lines( X, Y ) }.
% 101.23/101.60 parent0: (12011) {G1,W12,D2,L4,V3,M4} { unorthogonal_lines( X, Y ), !
% 101.23/101.60 convergent_lines( X, Z ), ! unorthogonal_lines( X, Z ), convergent_lines
% 101.23/101.60 ( Z, Y ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := X
% 101.23/101.60 Y := Z
% 101.23/101.60 Z := Y
% 101.23/101.60 end
% 101.23/101.60 permutation0:
% 101.23/101.60 0 ==> 2
% 101.23/101.60 1 ==> 0
% 101.23/101.60 2 ==> 3
% 101.23/101.60 3 ==> 1
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 resolution: (12013) {G1,W12,D2,L4,V3,M4} { convergent_lines( X, Y ), !
% 101.23/101.60 convergent_lines( X, Z ), ! unorthogonal_lines( X, Z ),
% 101.23/101.60 unorthogonal_lines( Z, Y ) }.
% 101.23/101.60 parent0[1]: (20) {G0,W6,D2,L2,V2,M1} I { convergent_lines( X, Y ), ! alpha1
% 101.23/101.60 ( X, Y ) }.
% 101.23/101.60 parent1[3]: (19) {G0,W12,D2,L4,V3,M1} I { ! convergent_lines( X, Y ), !
% 101.23/101.60 unorthogonal_lines( X, Y ), unorthogonal_lines( Y, Z ), alpha1( X, Z )
% 101.23/101.60 }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := X
% 101.23/101.60 Y := Y
% 101.23/101.60 end
% 101.23/101.60 substitution1:
% 101.23/101.60 X := X
% 101.23/101.60 Y := Z
% 101.23/101.60 Z := Y
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 subsumption: (264) {G1,W12,D2,L4,V3,M2} R(19,20) { ! convergent_lines( X, Y
% 101.23/101.60 ), convergent_lines( X, Z ), ! unorthogonal_lines( X, Y ),
% 101.23/101.60 unorthogonal_lines( Y, Z ) }.
% 101.23/101.60 parent0: (12013) {G1,W12,D2,L4,V3,M4} { convergent_lines( X, Y ), !
% 101.23/101.60 convergent_lines( X, Z ), ! unorthogonal_lines( X, Z ),
% 101.23/101.60 unorthogonal_lines( Z, Y ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := X
% 101.23/101.60 Y := Z
% 101.23/101.60 Z := Y
% 101.23/101.60 end
% 101.23/101.60 permutation0:
% 101.23/101.60 0 ==> 1
% 101.23/101.60 1 ==> 0
% 101.23/101.60 2 ==> 2
% 101.23/101.60 3 ==> 3
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 resolution: (12014) {G1,W16,D3,L4,V4,M4} { ! distinct_lines( Z,
% 101.23/101.60 orthogonal_through_point( X, Y ) ), apart_point_and_line( T, Z ),
% 101.23/101.60 apart_point_and_line( T, orthogonal_through_point( X, Y ) ),
% 101.23/101.60 unorthogonal_lines( Z, X ) }.
% 101.23/101.60 parent0[0]: (23) {G0,W5,D3,L1,V2,M1} I { ! unorthogonal_lines(
% 101.23/101.60 orthogonal_through_point( Y, X ), Y ) }.
% 101.23/101.60 parent1[3]: (25) {G0,W15,D2,L5,V4,M2} I { ! distinct_lines( X, Y ),
% 101.23/101.60 apart_point_and_line( Z, X ), apart_point_and_line( Z, Y ),
% 101.23/101.60 unorthogonal_lines( Y, T ), unorthogonal_lines( X, T ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := Y
% 101.23/101.60 Y := X
% 101.23/101.60 end
% 101.23/101.60 substitution1:
% 101.23/101.60 X := Z
% 101.23/101.60 Y := orthogonal_through_point( X, Y )
% 101.23/101.60 Z := T
% 101.23/101.60 T := X
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 subsumption: (299) {G1,W16,D3,L4,V4,M1} R(25,23) { ! distinct_lines( X,
% 101.23/101.60 orthogonal_through_point( Y, Z ) ), apart_point_and_line( T, X ),
% 101.23/101.60 apart_point_and_line( T, orthogonal_through_point( Y, Z ) ),
% 101.23/101.60 unorthogonal_lines( X, Y ) }.
% 101.23/101.60 parent0: (12014) {G1,W16,D3,L4,V4,M4} { ! distinct_lines( Z,
% 101.23/101.60 orthogonal_through_point( X, Y ) ), apart_point_and_line( T, Z ),
% 101.23/101.60 apart_point_and_line( T, orthogonal_through_point( X, Y ) ),
% 101.23/101.60 unorthogonal_lines( Z, X ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := Y
% 101.23/101.60 Y := Z
% 101.23/101.60 Z := X
% 101.23/101.60 T := T
% 101.23/101.60 end
% 101.23/101.60 permutation0:
% 101.23/101.60 0 ==> 0
% 101.23/101.60 1 ==> 1
% 101.23/101.60 2 ==> 2
% 101.23/101.60 3 ==> 3
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 resolution: (12018) {G1,W16,D3,L4,V4,M4} { ! distinct_lines(
% 101.23/101.60 orthogonal_through_point( X, Y ), Z ), apart_point_and_line( T,
% 101.23/101.60 orthogonal_through_point( X, Y ) ), apart_point_and_line( T, Z ),
% 101.23/101.60 unorthogonal_lines( Z, X ) }.
% 101.23/101.60 parent0[0]: (23) {G0,W5,D3,L1,V2,M1} I { ! unorthogonal_lines(
% 101.23/101.60 orthogonal_through_point( Y, X ), Y ) }.
% 101.23/101.60 parent1[4]: (25) {G0,W15,D2,L5,V4,M2} I { ! distinct_lines( X, Y ),
% 101.23/101.60 apart_point_and_line( Z, X ), apart_point_and_line( Z, Y ),
% 101.23/101.60 unorthogonal_lines( Y, T ), unorthogonal_lines( X, T ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := Y
% 101.23/101.60 Y := X
% 101.23/101.60 end
% 101.23/101.60 substitution1:
% 101.23/101.60 X := orthogonal_through_point( X, Y )
% 101.23/101.60 Y := Z
% 101.23/101.60 Z := T
% 101.23/101.60 T := X
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 subsumption: (300) {G1,W16,D3,L4,V4,M1} R(25,23) { ! distinct_lines(
% 101.23/101.60 orthogonal_through_point( X, Y ), Z ), apart_point_and_line( T,
% 101.23/101.60 orthogonal_through_point( X, Y ) ), apart_point_and_line( T, Z ),
% 101.23/101.60 unorthogonal_lines( Z, X ) }.
% 101.23/101.60 parent0: (12018) {G1,W16,D3,L4,V4,M4} { ! distinct_lines(
% 101.23/101.60 orthogonal_through_point( X, Y ), Z ), apart_point_and_line( T,
% 101.23/101.60 orthogonal_through_point( X, Y ) ), apart_point_and_line( T, Z ),
% 101.23/101.60 unorthogonal_lines( Z, X ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := X
% 101.23/101.60 Y := Y
% 101.23/101.60 Z := Z
% 101.23/101.60 T := T
% 101.23/101.60 end
% 101.23/101.60 permutation0:
% 101.23/101.60 0 ==> 0
% 101.23/101.60 1 ==> 1
% 101.23/101.60 2 ==> 2
% 101.23/101.60 3 ==> 3
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 resolution: (12020) {G1,W9,D4,L1,V0,M1} { distinct_lines(
% 101.23/101.60 orthogonal_through_point( orthogonal_through_point( skol2, skol1 ), skol1
% 101.23/101.60 ), parallel_through_point( skol2, skol1 ) ) }.
% 101.23/101.60 parent0[0]: (34) {G1,W6,D2,L2,V2,M2} R(4,1) { ! distinct_lines( Y, X ),
% 101.23/101.60 distinct_lines( X, Y ) }.
% 101.23/101.60 parent1[0]: (26) {G0,W9,D4,L1,V0,M1} I { distinct_lines(
% 101.23/101.60 parallel_through_point( skol2, skol1 ), orthogonal_through_point(
% 101.23/101.60 orthogonal_through_point( skol2, skol1 ), skol1 ) ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := orthogonal_through_point( orthogonal_through_point( skol2, skol1 )
% 101.23/101.60 , skol1 )
% 101.23/101.60 Y := parallel_through_point( skol2, skol1 )
% 101.23/101.60 end
% 101.23/101.60 substitution1:
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 subsumption: (318) {G2,W9,D4,L1,V0,M1} R(26,34) { distinct_lines(
% 101.23/101.60 orthogonal_through_point( orthogonal_through_point( skol2, skol1 ), skol1
% 101.23/101.60 ), parallel_through_point( skol2, skol1 ) ) }.
% 101.23/101.60 parent0: (12020) {G1,W9,D4,L1,V0,M1} { distinct_lines(
% 101.23/101.60 orthogonal_through_point( orthogonal_through_point( skol2, skol1 ), skol1
% 101.23/101.60 ), parallel_through_point( skol2, skol1 ) ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 end
% 101.23/101.60 permutation0:
% 101.23/101.60 0 ==> 0
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 resolution: (12021) {G1,W14,D3,L4,V5,M4} { distinct_lines( X,
% 101.23/101.60 orthogonal_through_point( Y, Z ) ), distinct_lines( T, X ),
% 101.23/101.60 distinct_lines( U, T ), ! apart_point_and_line( Z, U ) }.
% 101.23/101.60 parent0[2]: (198) {G2,W11,D3,L3,V4,M1} R(196,12) { distinct_lines( X,
% 101.23/101.60 orthogonal_through_point( Y, Z ) ), distinct_lines( T, X ), !
% 101.23/101.60 apart_point_and_line( Z, T ) }.
% 101.23/101.60 parent1[1]: (12) {G0,W9,D2,L3,V3,M2} I { distinct_lines( Y, Z ),
% 101.23/101.60 apart_point_and_line( X, Z ), ! apart_point_and_line( X, Y ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := X
% 101.23/101.60 Y := Y
% 101.23/101.60 Z := Z
% 101.23/101.60 T := T
% 101.23/101.60 end
% 101.23/101.60 substitution1:
% 101.23/101.60 X := Z
% 101.23/101.60 Y := U
% 101.23/101.60 Z := T
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 subsumption: (1826) {G3,W14,D3,L4,V5,M1} R(198,12) { distinct_lines( X,
% 101.23/101.60 orthogonal_through_point( Y, Z ) ), distinct_lines( T, X ),
% 101.23/101.60 distinct_lines( U, T ), ! apart_point_and_line( Z, U ) }.
% 101.23/101.60 parent0: (12021) {G1,W14,D3,L4,V5,M4} { distinct_lines( X,
% 101.23/101.60 orthogonal_through_point( Y, Z ) ), distinct_lines( T, X ),
% 101.23/101.60 distinct_lines( U, T ), ! apart_point_and_line( Z, U ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := X
% 101.23/101.60 Y := Y
% 101.23/101.60 Z := Z
% 101.23/101.60 T := T
% 101.23/101.60 U := U
% 101.23/101.60 end
% 101.23/101.60 permutation0:
% 101.23/101.60 0 ==> 0
% 101.23/101.60 1 ==> 1
% 101.23/101.60 2 ==> 2
% 101.23/101.60 3 ==> 3
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 factor: (12027) {G3,W13,D3,L3,V3,M3} { distinct_lines( X,
% 101.23/101.60 orthogonal_through_point( Y, Z ) ), distinct_lines(
% 101.23/101.60 orthogonal_through_point( Y, Z ), X ), ! apart_point_and_line( Z, X ) }.
% 101.23/101.60 parent0[0, 2]: (1826) {G3,W14,D3,L4,V5,M1} R(198,12) { distinct_lines( X,
% 101.23/101.60 orthogonal_through_point( Y, Z ) ), distinct_lines( T, X ),
% 101.23/101.60 distinct_lines( U, T ), ! apart_point_and_line( Z, U ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := X
% 101.23/101.60 Y := Y
% 101.23/101.60 Z := Z
% 101.23/101.60 T := orthogonal_through_point( Y, Z )
% 101.23/101.60 U := X
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 resolution: (12033) {G2,W13,D3,L3,V3,M3} { distinct_lines(
% 101.23/101.60 orthogonal_through_point( Y, Z ), X ), distinct_lines(
% 101.23/101.60 orthogonal_through_point( Y, Z ), X ), ! apart_point_and_line( Z, X ) }.
% 101.23/101.60 parent0[0]: (34) {G1,W6,D2,L2,V2,M2} R(4,1) { ! distinct_lines( Y, X ),
% 101.23/101.60 distinct_lines( X, Y ) }.
% 101.23/101.60 parent1[0]: (12027) {G3,W13,D3,L3,V3,M3} { distinct_lines( X,
% 101.23/101.60 orthogonal_through_point( Y, Z ) ), distinct_lines(
% 101.23/101.60 orthogonal_through_point( Y, Z ), X ), ! apart_point_and_line( Z, X ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := orthogonal_through_point( Y, Z )
% 101.23/101.60 Y := X
% 101.23/101.60 end
% 101.23/101.60 substitution1:
% 101.23/101.60 X := X
% 101.23/101.60 Y := Y
% 101.23/101.60 Z := Z
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 factor: (12035) {G2,W8,D3,L2,V3,M2} { distinct_lines(
% 101.23/101.60 orthogonal_through_point( X, Y ), Z ), ! apart_point_and_line( Y, Z ) }.
% 101.23/101.60 parent0[0, 1]: (12033) {G2,W13,D3,L3,V3,M3} { distinct_lines(
% 101.23/101.60 orthogonal_through_point( Y, Z ), X ), distinct_lines(
% 101.23/101.60 orthogonal_through_point( Y, Z ), X ), ! apart_point_and_line( Z, X ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := Z
% 101.23/101.60 Y := X
% 101.23/101.60 Z := Y
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 subsumption: (1828) {G4,W8,D3,L2,V3,M1} F(1826);r(34) { distinct_lines(
% 101.23/101.60 orthogonal_through_point( Y, Z ), X ), ! apart_point_and_line( Z, X ) }.
% 101.23/101.60 parent0: (12035) {G2,W8,D3,L2,V3,M2} { distinct_lines(
% 101.23/101.60 orthogonal_through_point( X, Y ), Z ), ! apart_point_and_line( Y, Z ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := Y
% 101.23/101.60 Y := Z
% 101.23/101.60 Z := X
% 101.23/101.60 end
% 101.23/101.60 permutation0:
% 101.23/101.60 0 ==> 0
% 101.23/101.60 1 ==> 1
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 resolution: (12037) {G1,W13,D3,L3,V3,M3} { ! convergent_lines(
% 101.23/101.60 orthogonal_through_point( X, Y ), Z ), convergent_lines( Z, X ), !
% 101.23/101.60 unorthogonal_lines( orthogonal_through_point( X, Y ), Z ) }.
% 101.23/101.60 parent0[0]: (23) {G0,W5,D3,L1,V2,M1} I { ! unorthogonal_lines(
% 101.23/101.60 orthogonal_through_point( Y, X ), Y ) }.
% 101.23/101.60 parent1[2]: (241) {G1,W12,D2,L4,V3,M2} R(18,21) { ! convergent_lines( X, Y
% 101.23/101.60 ), convergent_lines( Y, Z ), unorthogonal_lines( X, Z ), !
% 101.23/101.60 unorthogonal_lines( X, Y ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := Y
% 101.23/101.60 Y := X
% 101.23/101.60 end
% 101.23/101.60 substitution1:
% 101.23/101.60 X := orthogonal_through_point( X, Y )
% 101.23/101.60 Y := Z
% 101.23/101.60 Z := X
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 resolution: (12039) {G2,W11,D3,L3,V3,M3} { convergent_lines( Z, X ), !
% 101.23/101.60 unorthogonal_lines( orthogonal_through_point( X, Y ), Z ),
% 101.23/101.60 convergent_lines( Z, X ) }.
% 101.23/101.60 parent0[0]: (12037) {G1,W13,D3,L3,V3,M3} { ! convergent_lines(
% 101.23/101.60 orthogonal_through_point( X, Y ), Z ), convergent_lines( Z, X ), !
% 101.23/101.60 unorthogonal_lines( orthogonal_through_point( X, Y ), Z ) }.
% 101.23/101.60 parent1[1]: (93) {G3,W8,D3,L2,V3,M2} R(40,43) { convergent_lines( Z, X ),
% 101.23/101.60 convergent_lines( orthogonal_through_point( X, Y ), Z ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := X
% 101.23/101.60 Y := Y
% 101.23/101.60 Z := Z
% 101.23/101.60 end
% 101.23/101.60 substitution1:
% 101.23/101.60 X := X
% 101.23/101.60 Y := Y
% 101.23/101.60 Z := Z
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 factor: (12040) {G2,W8,D3,L2,V3,M2} { convergent_lines( X, Y ), !
% 101.23/101.60 unorthogonal_lines( orthogonal_through_point( Y, Z ), X ) }.
% 101.23/101.60 parent0[0, 2]: (12039) {G2,W11,D3,L3,V3,M3} { convergent_lines( Z, X ), !
% 101.23/101.60 unorthogonal_lines( orthogonal_through_point( X, Y ), Z ),
% 101.23/101.60 convergent_lines( Z, X ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := Y
% 101.23/101.60 Y := Z
% 101.23/101.60 Z := X
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 subsumption: (2975) {G4,W8,D3,L2,V3,M1} R(241,23);r(93) { convergent_lines
% 101.23/101.60 ( Z, X ), ! unorthogonal_lines( orthogonal_through_point( X, Y ), Z ) }.
% 101.23/101.60 parent0: (12040) {G2,W8,D3,L2,V3,M2} { convergent_lines( X, Y ), !
% 101.23/101.60 unorthogonal_lines( orthogonal_through_point( Y, Z ), X ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := Z
% 101.23/101.60 Y := X
% 101.23/101.60 Z := Y
% 101.23/101.60 end
% 101.23/101.60 permutation0:
% 101.23/101.60 0 ==> 0
% 101.23/101.60 1 ==> 1
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 resolution: (12041) {G2,W16,D3,L4,V4,M4} { convergent_lines( X, Y ), !
% 101.23/101.60 convergent_lines( T, orthogonal_through_point( Y, Z ) ), convergent_lines
% 101.23/101.60 ( T, X ), ! unorthogonal_lines( T, orthogonal_through_point( Y, Z ) ) }.
% 101.23/101.60 parent0[1]: (2975) {G4,W8,D3,L2,V3,M1} R(241,23);r(93) { convergent_lines(
% 101.23/101.60 Z, X ), ! unorthogonal_lines( orthogonal_through_point( X, Y ), Z ) }.
% 101.23/101.60 parent1[3]: (264) {G1,W12,D2,L4,V3,M2} R(19,20) { ! convergent_lines( X, Y
% 101.23/101.60 ), convergent_lines( X, Z ), ! unorthogonal_lines( X, Y ),
% 101.23/101.60 unorthogonal_lines( Y, Z ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := Y
% 101.23/101.60 Y := Z
% 101.23/101.60 Z := X
% 101.23/101.60 end
% 101.23/101.60 substitution1:
% 101.23/101.60 X := T
% 101.23/101.60 Y := orthogonal_through_point( Y, Z )
% 101.23/101.60 Z := X
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 subsumption: (2979) {G5,W16,D3,L4,V4,M1} R(2975,264) { convergent_lines( X
% 101.23/101.60 , Y ), ! convergent_lines( Z, orthogonal_through_point( Y, T ) ),
% 101.23/101.60 convergent_lines( Z, X ), ! unorthogonal_lines( Z,
% 101.23/101.60 orthogonal_through_point( Y, T ) ) }.
% 101.23/101.60 parent0: (12041) {G2,W16,D3,L4,V4,M4} { convergent_lines( X, Y ), !
% 101.23/101.60 convergent_lines( T, orthogonal_through_point( Y, Z ) ), convergent_lines
% 101.23/101.60 ( T, X ), ! unorthogonal_lines( T, orthogonal_through_point( Y, Z ) ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := X
% 101.23/101.60 Y := Y
% 101.23/101.60 Z := T
% 101.23/101.60 T := Z
% 101.23/101.60 end
% 101.23/101.60 permutation0:
% 101.23/101.60 0 ==> 0
% 101.23/101.60 1 ==> 1
% 101.23/101.60 2 ==> 2
% 101.23/101.60 3 ==> 3
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 factor: (12043) {G5,W13,D3,L3,V2,M3} { convergent_lines( X, X ), !
% 101.23/101.60 convergent_lines( X, orthogonal_through_point( X, Y ) ), !
% 101.23/101.60 unorthogonal_lines( X, orthogonal_through_point( X, Y ) ) }.
% 101.23/101.60 parent0[0, 2]: (2979) {G5,W16,D3,L4,V4,M1} R(2975,264) { convergent_lines(
% 101.23/101.60 X, Y ), ! convergent_lines( Z, orthogonal_through_point( Y, T ) ),
% 101.23/101.60 convergent_lines( Z, X ), ! unorthogonal_lines( Z,
% 101.23/101.60 orthogonal_through_point( Y, T ) ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := X
% 101.23/101.60 Y := X
% 101.23/101.60 Z := X
% 101.23/101.60 T := Y
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 resolution: (12044) {G1,W10,D3,L2,V2,M2} { ! convergent_lines( X,
% 101.23/101.60 orthogonal_through_point( X, Y ) ), ! unorthogonal_lines( X,
% 101.23/101.60 orthogonal_through_point( X, Y ) ) }.
% 101.23/101.60 parent0[0]: (2) {G0,W3,D2,L1,V1,M1} I { ! convergent_lines( X, X ) }.
% 101.23/101.60 parent1[0]: (12043) {G5,W13,D3,L3,V2,M3} { convergent_lines( X, X ), !
% 101.23/101.60 convergent_lines( X, orthogonal_through_point( X, Y ) ), !
% 101.23/101.60 unorthogonal_lines( X, orthogonal_through_point( X, Y ) ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := X
% 101.23/101.60 end
% 101.23/101.60 substitution1:
% 101.23/101.60 X := X
% 101.23/101.60 Y := Y
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 subsumption: (2980) {G6,W10,D3,L2,V2,M1} F(2979);r(2) { ! convergent_lines
% 101.23/101.60 ( X, orthogonal_through_point( X, Y ) ), ! unorthogonal_lines( X,
% 101.23/101.60 orthogonal_through_point( X, Y ) ) }.
% 101.23/101.60 parent0: (12044) {G1,W10,D3,L2,V2,M2} { ! convergent_lines( X,
% 101.23/101.60 orthogonal_through_point( X, Y ) ), ! unorthogonal_lines( X,
% 101.23/101.60 orthogonal_through_point( X, Y ) ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := X
% 101.23/101.60 Y := Y
% 101.23/101.60 end
% 101.23/101.60 permutation0:
% 101.23/101.60 0 ==> 0
% 101.23/101.60 1 ==> 1
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 resolution: (12045) {G3,W5,D3,L1,V2,M1} { ! unorthogonal_lines( X,
% 101.23/101.60 orthogonal_through_point( X, Y ) ) }.
% 101.23/101.60 parent0[0]: (2980) {G6,W10,D3,L2,V2,M1} F(2979);r(2) { ! convergent_lines(
% 101.23/101.60 X, orthogonal_through_point( X, Y ) ), ! unorthogonal_lines( X,
% 101.23/101.60 orthogonal_through_point( X, Y ) ) }.
% 101.23/101.60 parent1[0]: (46) {G2,W5,D3,L1,V2,M1} R(43,37) { convergent_lines( X,
% 101.23/101.60 orthogonal_through_point( X, Y ) ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := X
% 101.23/101.60 Y := Y
% 101.23/101.60 end
% 101.23/101.60 substitution1:
% 101.23/101.60 X := X
% 101.23/101.60 Y := Y
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 subsumption: (2981) {G7,W5,D3,L1,V2,M1} S(2980);r(46) { !
% 101.23/101.60 unorthogonal_lines( X, orthogonal_through_point( X, Y ) ) }.
% 101.23/101.60 parent0: (12045) {G3,W5,D3,L1,V2,M1} { ! unorthogonal_lines( X,
% 101.23/101.60 orthogonal_through_point( X, Y ) ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := X
% 101.23/101.60 Y := Y
% 101.23/101.60 end
% 101.23/101.60 permutation0:
% 101.23/101.60 0 ==> 0
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 resolution: (12046) {G1,W14,D3,L2,V3,M2} { convergent_lines(
% 101.23/101.60 orthogonal_through_point( Y, X ), parallel_through_point( Z, X ) ), !
% 101.23/101.60 distinct_lines( orthogonal_through_point( Y, X ), parallel_through_point
% 101.23/101.60 ( Z, X ) ) }.
% 101.23/101.60 parent0[0]: (24) {G0,W5,D3,L1,V2,M1} I { ! apart_point_and_line( X,
% 101.23/101.60 orthogonal_through_point( Y, X ) ) }.
% 101.23/101.60 parent1[2]: (226) {G1,W13,D3,L3,V3,M1} R(16,15) { convergent_lines( X,
% 101.23/101.60 parallel_through_point( Y, Z ) ), ! distinct_lines( X,
% 101.23/101.60 parallel_through_point( Y, Z ) ), apart_point_and_line( Z, X ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := X
% 101.23/101.60 Y := Y
% 101.23/101.60 end
% 101.23/101.60 substitution1:
% 101.23/101.60 X := orthogonal_through_point( Y, X )
% 101.23/101.60 Y := Z
% 101.23/101.60 Z := X
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 subsumption: (4470) {G2,W14,D3,L2,V3,M1} R(226,24) { convergent_lines(
% 101.23/101.60 orthogonal_through_point( X, Y ), parallel_through_point( Z, Y ) ), !
% 101.23/101.60 distinct_lines( orthogonal_through_point( X, Y ), parallel_through_point
% 101.23/101.60 ( Z, Y ) ) }.
% 101.23/101.60 parent0: (12046) {G1,W14,D3,L2,V3,M2} { convergent_lines(
% 101.23/101.60 orthogonal_through_point( Y, X ), parallel_through_point( Z, X ) ), !
% 101.23/101.60 distinct_lines( orthogonal_through_point( Y, X ), parallel_through_point
% 101.23/101.60 ( Z, X ) ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := Y
% 101.23/101.60 Y := X
% 101.23/101.60 Z := Z
% 101.23/101.60 end
% 101.23/101.60 permutation0:
% 101.23/101.60 0 ==> 0
% 101.23/101.60 1 ==> 1
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 resolution: (12047) {G1,W17,D3,L3,V4,M3} { ! distinct_lines(
% 101.23/101.60 orthogonal_through_point( X, Y ), orthogonal_through_point( X, Z ) ),
% 101.23/101.60 apart_point_and_line( T, orthogonal_through_point( X, Y ) ),
% 101.23/101.60 apart_point_and_line( T, orthogonal_through_point( X, Z ) ) }.
% 101.23/101.60 parent0[0]: (23) {G0,W5,D3,L1,V2,M1} I { ! unorthogonal_lines(
% 101.23/101.60 orthogonal_through_point( Y, X ), Y ) }.
% 101.23/101.60 parent1[3]: (299) {G1,W16,D3,L4,V4,M1} R(25,23) { ! distinct_lines( X,
% 101.23/101.60 orthogonal_through_point( Y, Z ) ), apart_point_and_line( T, X ),
% 101.23/101.60 apart_point_and_line( T, orthogonal_through_point( Y, Z ) ),
% 101.23/101.60 unorthogonal_lines( X, Y ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := Y
% 101.23/101.60 Y := X
% 101.23/101.60 end
% 101.23/101.60 substitution1:
% 101.23/101.60 X := orthogonal_through_point( X, Y )
% 101.23/101.60 Y := X
% 101.23/101.60 Z := Z
% 101.23/101.60 T := T
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 subsumption: (4483) {G2,W17,D3,L3,V4,M2} R(299,23) { ! distinct_lines(
% 101.23/101.60 orthogonal_through_point( X, Y ), orthogonal_through_point( X, Z ) ),
% 101.23/101.60 apart_point_and_line( T, orthogonal_through_point( X, Z ) ),
% 101.23/101.60 apart_point_and_line( T, orthogonal_through_point( X, Y ) ) }.
% 101.23/101.60 parent0: (12047) {G1,W17,D3,L3,V4,M3} { ! distinct_lines(
% 101.23/101.60 orthogonal_through_point( X, Y ), orthogonal_through_point( X, Z ) ),
% 101.23/101.60 apart_point_and_line( T, orthogonal_through_point( X, Y ) ),
% 101.23/101.60 apart_point_and_line( T, orthogonal_through_point( X, Z ) ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := X
% 101.23/101.60 Y := Y
% 101.23/101.60 Z := Z
% 101.23/101.60 T := T
% 101.23/101.60 end
% 101.23/101.60 permutation0:
% 101.23/101.60 0 ==> 0
% 101.23/101.60 1 ==> 2
% 101.23/101.60 2 ==> 1
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 resolution: (12049) {G2,W17,D4,L3,V4,M3} { ! distinct_lines(
% 101.23/101.60 orthogonal_through_point( orthogonal_through_point( X, Y ), Z ), X ),
% 101.23/101.60 apart_point_and_line( T, orthogonal_through_point(
% 101.23/101.60 orthogonal_through_point( X, Y ), Z ) ), apart_point_and_line( T, X ) }.
% 101.23/101.60 parent0[0]: (2981) {G7,W5,D3,L1,V2,M1} S(2980);r(46) { ! unorthogonal_lines
% 101.23/101.60 ( X, orthogonal_through_point( X, Y ) ) }.
% 101.23/101.60 parent1[3]: (300) {G1,W16,D3,L4,V4,M1} R(25,23) { ! distinct_lines(
% 101.23/101.60 orthogonal_through_point( X, Y ), Z ), apart_point_and_line( T,
% 101.23/101.60 orthogonal_through_point( X, Y ) ), apart_point_and_line( T, Z ),
% 101.23/101.60 unorthogonal_lines( Z, X ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := X
% 101.23/101.60 Y := Y
% 101.23/101.60 end
% 101.23/101.60 substitution1:
% 101.23/101.60 X := orthogonal_through_point( X, Y )
% 101.23/101.60 Y := Z
% 101.23/101.60 Z := X
% 101.23/101.60 T := T
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 subsumption: (4484) {G8,W17,D4,L3,V4,M2} R(300,2981) { ! distinct_lines(
% 101.23/101.60 orthogonal_through_point( orthogonal_through_point( X, Y ), Z ), X ),
% 101.23/101.60 apart_point_and_line( T, X ), apart_point_and_line( T,
% 101.23/101.60 orthogonal_through_point( orthogonal_through_point( X, Y ), Z ) ) }.
% 101.23/101.60 parent0: (12049) {G2,W17,D4,L3,V4,M3} { ! distinct_lines(
% 101.23/101.60 orthogonal_through_point( orthogonal_through_point( X, Y ), Z ), X ),
% 101.23/101.60 apart_point_and_line( T, orthogonal_through_point(
% 101.23/101.60 orthogonal_through_point( X, Y ), Z ) ), apart_point_and_line( T, X ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := X
% 101.23/101.60 Y := Y
% 101.23/101.60 Z := Z
% 101.23/101.60 T := T
% 101.23/101.60 end
% 101.23/101.60 permutation0:
% 101.23/101.60 0 ==> 0
% 101.23/101.60 1 ==> 2
% 101.23/101.60 2 ==> 1
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 resolution: (12050) {G3,W9,D4,L1,V0,M1} { convergent_lines(
% 101.23/101.60 orthogonal_through_point( orthogonal_through_point( skol2, skol1 ), skol1
% 101.23/101.60 ), parallel_through_point( skol2, skol1 ) ) }.
% 101.23/101.60 parent0[1]: (4470) {G2,W14,D3,L2,V3,M1} R(226,24) { convergent_lines(
% 101.23/101.60 orthogonal_through_point( X, Y ), parallel_through_point( Z, Y ) ), !
% 101.23/101.60 distinct_lines( orthogonal_through_point( X, Y ), parallel_through_point
% 101.23/101.60 ( Z, Y ) ) }.
% 101.23/101.60 parent1[0]: (318) {G2,W9,D4,L1,V0,M1} R(26,34) { distinct_lines(
% 101.23/101.60 orthogonal_through_point( orthogonal_through_point( skol2, skol1 ), skol1
% 101.23/101.60 ), parallel_through_point( skol2, skol1 ) ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := orthogonal_through_point( skol2, skol1 )
% 101.23/101.60 Y := skol1
% 101.23/101.60 Z := skol2
% 101.23/101.60 end
% 101.23/101.60 substitution1:
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 subsumption: (4893) {G3,W9,D4,L1,V0,M1} R(4470,318) { convergent_lines(
% 101.23/101.60 orthogonal_through_point( orthogonal_through_point( skol2, skol1 ), skol1
% 101.23/101.60 ), parallel_through_point( skol2, skol1 ) ) }.
% 101.23/101.60 parent0: (12050) {G3,W9,D4,L1,V0,M1} { convergent_lines(
% 101.23/101.60 orthogonal_through_point( orthogonal_through_point( skol2, skol1 ), skol1
% 101.23/101.60 ), parallel_through_point( skol2, skol1 ) ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 end
% 101.23/101.60 permutation0:
% 101.23/101.60 0 ==> 0
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 resolution: (12051) {G3,W10,D4,L2,V1,M2} { convergent_lines(
% 101.23/101.60 orthogonal_through_point( orthogonal_through_point( skol2, skol1 ), skol1
% 101.23/101.60 ), X ), convergent_lines( X, skol2 ) }.
% 101.23/101.60 parent0[1]: (151) {G2,W11,D3,L3,V4,M3} R(41,5) { convergent_lines( Z, X ),
% 101.23/101.60 ! convergent_lines( Z, parallel_through_point( Y, T ) ), convergent_lines
% 101.23/101.60 ( X, Y ) }.
% 101.23/101.60 parent1[0]: (4893) {G3,W9,D4,L1,V0,M1} R(4470,318) { convergent_lines(
% 101.23/101.60 orthogonal_through_point( orthogonal_through_point( skol2, skol1 ), skol1
% 101.23/101.60 ), parallel_through_point( skol2, skol1 ) ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := X
% 101.23/101.60 Y := skol2
% 101.23/101.60 Z := orthogonal_through_point( orthogonal_through_point( skol2, skol1 )
% 101.23/101.60 , skol1 )
% 101.23/101.60 T := skol1
% 101.23/101.60 end
% 101.23/101.60 substitution1:
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 subsumption: (4979) {G4,W10,D4,L2,V1,M2} R(4893,151) { convergent_lines( X
% 101.23/101.60 , skol2 ), convergent_lines( orthogonal_through_point(
% 101.23/101.60 orthogonal_through_point( skol2, skol1 ), skol1 ), X ) }.
% 101.23/101.60 parent0: (12051) {G3,W10,D4,L2,V1,M2} { convergent_lines(
% 101.23/101.60 orthogonal_through_point( orthogonal_through_point( skol2, skol1 ), skol1
% 101.23/101.60 ), X ), convergent_lines( X, skol2 ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := X
% 101.23/101.60 end
% 101.23/101.60 permutation0:
% 101.23/101.60 0 ==> 1
% 101.23/101.60 1 ==> 0
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 resolution: (12053) {G1,W12,D3,L2,V3,M2} { ! distinct_lines(
% 101.23/101.60 orthogonal_through_point( Y, X ), orthogonal_through_point( Y, Z ) ),
% 101.23/101.60 apart_point_and_line( X, orthogonal_through_point( Y, Z ) ) }.
% 101.23/101.60 parent0[0]: (24) {G0,W5,D3,L1,V2,M1} I { ! apart_point_and_line( X,
% 101.23/101.60 orthogonal_through_point( Y, X ) ) }.
% 101.23/101.60 parent1[2]: (4483) {G2,W17,D3,L3,V4,M2} R(299,23) { ! distinct_lines(
% 101.23/101.60 orthogonal_through_point( X, Y ), orthogonal_through_point( X, Z ) ),
% 101.23/101.60 apart_point_and_line( T, orthogonal_through_point( X, Z ) ),
% 101.23/101.60 apart_point_and_line( T, orthogonal_through_point( X, Y ) ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := X
% 101.23/101.60 Y := Y
% 101.23/101.60 end
% 101.23/101.60 substitution1:
% 101.23/101.60 X := Y
% 101.23/101.60 Y := X
% 101.23/101.60 Z := Z
% 101.23/101.60 T := X
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 subsumption: (5959) {G3,W12,D3,L2,V3,M1} R(4483,24) { ! distinct_lines(
% 101.23/101.60 orthogonal_through_point( X, Y ), orthogonal_through_point( X, Z ) ),
% 101.23/101.60 apart_point_and_line( Y, orthogonal_through_point( X, Z ) ) }.
% 101.23/101.60 parent0: (12053) {G1,W12,D3,L2,V3,M2} { ! distinct_lines(
% 101.23/101.60 orthogonal_through_point( Y, X ), orthogonal_through_point( Y, Z ) ),
% 101.23/101.60 apart_point_and_line( X, orthogonal_through_point( Y, Z ) ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := Y
% 101.23/101.60 Y := X
% 101.23/101.60 Z := Z
% 101.23/101.60 end
% 101.23/101.60 permutation0:
% 101.23/101.60 0 ==> 0
% 101.23/101.60 1 ==> 1
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 resolution: (12055) {G4,W14,D3,L2,V4,M2} { distinct_lines(
% 101.23/101.60 orthogonal_through_point( X, Y ), orthogonal_through_point( Z, T ) ), !
% 101.23/101.60 distinct_lines( orthogonal_through_point( Z, Y ),
% 101.23/101.60 orthogonal_through_point( Z, T ) ) }.
% 101.23/101.60 parent0[1]: (1828) {G4,W8,D3,L2,V3,M1} F(1826);r(34) { distinct_lines(
% 101.23/101.60 orthogonal_through_point( Y, Z ), X ), ! apart_point_and_line( Z, X ) }.
% 101.23/101.60 parent1[1]: (5959) {G3,W12,D3,L2,V3,M1} R(4483,24) { ! distinct_lines(
% 101.23/101.60 orthogonal_through_point( X, Y ), orthogonal_through_point( X, Z ) ),
% 101.23/101.60 apart_point_and_line( Y, orthogonal_through_point( X, Z ) ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := orthogonal_through_point( Z, T )
% 101.23/101.60 Y := X
% 101.23/101.60 Z := Y
% 101.23/101.60 end
% 101.23/101.60 substitution1:
% 101.23/101.60 X := Z
% 101.23/101.60 Y := Y
% 101.23/101.60 Z := T
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 subsumption: (6189) {G5,W14,D3,L2,V4,M2} R(5959,1828) { distinct_lines(
% 101.23/101.60 orthogonal_through_point( T, Y ), orthogonal_through_point( X, Z ) ), !
% 101.23/101.60 distinct_lines( orthogonal_through_point( X, Y ),
% 101.23/101.60 orthogonal_through_point( X, Z ) ) }.
% 101.23/101.60 parent0: (12055) {G4,W14,D3,L2,V4,M2} { distinct_lines(
% 101.23/101.60 orthogonal_through_point( X, Y ), orthogonal_through_point( Z, T ) ), !
% 101.23/101.60 distinct_lines( orthogonal_through_point( Z, Y ),
% 101.23/101.60 orthogonal_through_point( Z, T ) ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := T
% 101.23/101.60 Y := Y
% 101.23/101.60 Z := X
% 101.23/101.60 T := Z
% 101.23/101.60 end
% 101.23/101.60 permutation0:
% 101.23/101.60 0 ==> 0
% 101.23/101.60 1 ==> 1
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 resolution: (12056) {G3,W16,D5,L2,V3,M2} { ! convergent_lines( X,
% 101.23/101.60 orthogonal_through_point( Y, Z ) ), ! distinct_lines(
% 101.23/101.60 orthogonal_through_point( Y, intersection_point( X,
% 101.23/101.60 orthogonal_through_point( Y, Z ) ) ), orthogonal_through_point( Y, Z ) )
% 101.23/101.60 }.
% 101.23/101.60 parent0[1]: (176) {G2,W8,D3,L2,V2,M1} F(167);r(0) { ! convergent_lines( X,
% 101.23/101.60 Y ), ! apart_point_and_line( intersection_point( X, Y ), Y ) }.
% 101.23/101.60 parent1[1]: (5959) {G3,W12,D3,L2,V3,M1} R(4483,24) { ! distinct_lines(
% 101.23/101.60 orthogonal_through_point( X, Y ), orthogonal_through_point( X, Z ) ),
% 101.23/101.60 apart_point_and_line( Y, orthogonal_through_point( X, Z ) ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := X
% 101.23/101.60 Y := orthogonal_through_point( Y, Z )
% 101.23/101.60 end
% 101.23/101.60 substitution1:
% 101.23/101.60 X := Y
% 101.23/101.60 Y := intersection_point( X, orthogonal_through_point( Y, Z ) )
% 101.23/101.60 Z := Z
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 subsumption: (6192) {G4,W16,D5,L2,V3,M1} R(5959,176) { ! convergent_lines(
% 101.23/101.60 Y, orthogonal_through_point( X, Z ) ), ! distinct_lines(
% 101.23/101.60 orthogonal_through_point( X, intersection_point( Y,
% 101.23/101.60 orthogonal_through_point( X, Z ) ) ), orthogonal_through_point( X, Z ) )
% 101.23/101.60 }.
% 101.23/101.60 parent0: (12056) {G3,W16,D5,L2,V3,M2} { ! convergent_lines( X,
% 101.23/101.60 orthogonal_through_point( Y, Z ) ), ! distinct_lines(
% 101.23/101.60 orthogonal_through_point( Y, intersection_point( X,
% 101.23/101.60 orthogonal_through_point( Y, Z ) ) ), orthogonal_through_point( Y, Z ) )
% 101.23/101.60 }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := Y
% 101.23/101.60 Y := X
% 101.23/101.60 Z := Z
% 101.23/101.60 end
% 101.23/101.60 permutation0:
% 101.23/101.60 0 ==> 0
% 101.23/101.60 1 ==> 1
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 resolution: (12057) {G1,W14,D3,L2,V4,M2} { distinct_lines(
% 101.23/101.60 orthogonal_through_point( X, Y ), orthogonal_through_point( Z, T ) ), !
% 101.23/101.60 convergent_lines( orthogonal_through_point( Z, Y ),
% 101.23/101.60 orthogonal_through_point( Z, T ) ) }.
% 101.23/101.60 parent0[1]: (6189) {G5,W14,D3,L2,V4,M2} R(5959,1828) { distinct_lines(
% 101.23/101.60 orthogonal_through_point( T, Y ), orthogonal_through_point( X, Z ) ), !
% 101.23/101.60 distinct_lines( orthogonal_through_point( X, Y ),
% 101.23/101.60 orthogonal_through_point( X, Z ) ) }.
% 101.23/101.60 parent1[1]: (13) {G0,W6,D2,L2,V2,M1} I { ! convergent_lines( X, Y ),
% 101.23/101.60 distinct_lines( X, Y ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := Z
% 101.23/101.60 Y := Y
% 101.23/101.60 Z := T
% 101.23/101.60 T := X
% 101.23/101.60 end
% 101.23/101.60 substitution1:
% 101.23/101.60 X := orthogonal_through_point( Z, Y )
% 101.23/101.60 Y := orthogonal_through_point( Z, T )
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 subsumption: (6301) {G6,W14,D3,L2,V4,M1} R(6189,13) { ! convergent_lines(
% 101.23/101.60 orthogonal_through_point( Z, Y ), orthogonal_through_point( Z, T ) ),
% 101.23/101.60 distinct_lines( orthogonal_through_point( X, Y ),
% 101.23/101.60 orthogonal_through_point( Z, T ) ) }.
% 101.23/101.60 parent0: (12057) {G1,W14,D3,L2,V4,M2} { distinct_lines(
% 101.23/101.60 orthogonal_through_point( X, Y ), orthogonal_through_point( Z, T ) ), !
% 101.23/101.60 convergent_lines( orthogonal_through_point( Z, Y ),
% 101.23/101.60 orthogonal_through_point( Z, T ) ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := X
% 101.23/101.60 Y := Y
% 101.23/101.60 Z := Z
% 101.23/101.60 T := T
% 101.23/101.60 end
% 101.23/101.60 permutation0:
% 101.23/101.60 0 ==> 1
% 101.23/101.60 1 ==> 0
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 resolution: (12058) {G2,W14,D3,L2,V4,M2} { distinct_lines(
% 101.23/101.60 orthogonal_through_point( Z, T ), orthogonal_through_point( X, Y ) ), !
% 101.23/101.60 convergent_lines( orthogonal_through_point( Z, Y ),
% 101.23/101.60 orthogonal_through_point( Z, T ) ) }.
% 101.23/101.60 parent0[0]: (34) {G1,W6,D2,L2,V2,M2} R(4,1) { ! distinct_lines( Y, X ),
% 101.23/101.60 distinct_lines( X, Y ) }.
% 101.23/101.60 parent1[1]: (6301) {G6,W14,D3,L2,V4,M1} R(6189,13) { ! convergent_lines(
% 101.23/101.60 orthogonal_through_point( Z, Y ), orthogonal_through_point( Z, T ) ),
% 101.23/101.60 distinct_lines( orthogonal_through_point( X, Y ),
% 101.23/101.60 orthogonal_through_point( Z, T ) ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := orthogonal_through_point( Z, T )
% 101.23/101.60 Y := orthogonal_through_point( X, Y )
% 101.23/101.60 end
% 101.23/101.60 substitution1:
% 101.23/101.60 X := X
% 101.23/101.60 Y := Y
% 101.23/101.60 Z := Z
% 101.23/101.60 T := T
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 subsumption: (6346) {G7,W14,D3,L2,V4,M1} R(6301,34) { ! convergent_lines(
% 101.23/101.60 orthogonal_through_point( X, Y ), orthogonal_through_point( X, Z ) ),
% 101.23/101.60 distinct_lines( orthogonal_through_point( X, Z ),
% 101.23/101.60 orthogonal_through_point( T, Y ) ) }.
% 101.23/101.60 parent0: (12058) {G2,W14,D3,L2,V4,M2} { distinct_lines(
% 101.23/101.60 orthogonal_through_point( Z, T ), orthogonal_through_point( X, Y ) ), !
% 101.23/101.60 convergent_lines( orthogonal_through_point( Z, Y ),
% 101.23/101.60 orthogonal_through_point( Z, T ) ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := T
% 101.23/101.60 Y := Y
% 101.23/101.60 Z := X
% 101.23/101.60 T := Z
% 101.23/101.60 end
% 101.23/101.60 permutation0:
% 101.23/101.60 0 ==> 1
% 101.23/101.60 1 ==> 0
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 resolution: (12059) {G5,W16,D5,L2,V3,M2} { ! convergent_lines( X,
% 101.23/101.60 orthogonal_through_point( Y, Z ) ), ! convergent_lines(
% 101.23/101.60 orthogonal_through_point( Y, Z ), orthogonal_through_point( Y,
% 101.23/101.60 intersection_point( X, orthogonal_through_point( Y, Z ) ) ) ) }.
% 101.23/101.60 parent0[1]: (6192) {G4,W16,D5,L2,V3,M1} R(5959,176) { ! convergent_lines( Y
% 101.23/101.60 , orthogonal_through_point( X, Z ) ), ! distinct_lines(
% 101.23/101.60 orthogonal_through_point( X, intersection_point( Y,
% 101.23/101.60 orthogonal_through_point( X, Z ) ) ), orthogonal_through_point( X, Z ) )
% 101.23/101.60 }.
% 101.23/101.60 parent1[1]: (6346) {G7,W14,D3,L2,V4,M1} R(6301,34) { ! convergent_lines(
% 101.23/101.60 orthogonal_through_point( X, Y ), orthogonal_through_point( X, Z ) ),
% 101.23/101.60 distinct_lines( orthogonal_through_point( X, Z ),
% 101.23/101.60 orthogonal_through_point( T, Y ) ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := Y
% 101.23/101.60 Y := X
% 101.23/101.60 Z := Z
% 101.23/101.60 end
% 101.23/101.60 substitution1:
% 101.23/101.60 X := Y
% 101.23/101.60 Y := Z
% 101.23/101.60 Z := intersection_point( X, orthogonal_through_point( Y, Z ) )
% 101.23/101.60 T := Y
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 subsumption: (6984) {G8,W16,D5,L2,V3,M2} R(6192,6346) { ! convergent_lines
% 101.23/101.60 ( orthogonal_through_point( Y, Z ), orthogonal_through_point( Y,
% 101.23/101.60 intersection_point( X, orthogonal_through_point( Y, Z ) ) ) ), !
% 101.23/101.60 convergent_lines( X, orthogonal_through_point( Y, Z ) ) }.
% 101.23/101.60 parent0: (12059) {G5,W16,D5,L2,V3,M2} { ! convergent_lines( X,
% 101.23/101.60 orthogonal_through_point( Y, Z ) ), ! convergent_lines(
% 101.23/101.60 orthogonal_through_point( Y, Z ), orthogonal_through_point( Y,
% 101.23/101.60 intersection_point( X, orthogonal_through_point( Y, Z ) ) ) ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := X
% 101.23/101.60 Y := Y
% 101.23/101.60 Z := Z
% 101.23/101.60 end
% 101.23/101.60 permutation0:
% 101.23/101.60 0 ==> 1
% 101.23/101.60 1 ==> 0
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 resolution: (12060) {G3,W11,D5,L1,V2,M1} { ! convergent_lines(
% 101.23/101.60 orthogonal_through_point( X, Y ), orthogonal_through_point( X,
% 101.23/101.60 intersection_point( X, orthogonal_through_point( X, Y ) ) ) ) }.
% 101.23/101.60 parent0[1]: (6984) {G8,W16,D5,L2,V3,M2} R(6192,6346) { ! convergent_lines(
% 101.23/101.60 orthogonal_through_point( Y, Z ), orthogonal_through_point( Y,
% 101.23/101.60 intersection_point( X, orthogonal_through_point( Y, Z ) ) ) ), !
% 101.23/101.60 convergent_lines( X, orthogonal_through_point( Y, Z ) ) }.
% 101.23/101.60 parent1[0]: (46) {G2,W5,D3,L1,V2,M1} R(43,37) { convergent_lines( X,
% 101.23/101.60 orthogonal_through_point( X, Y ) ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := X
% 101.23/101.60 Y := X
% 101.23/101.60 Z := Y
% 101.23/101.60 end
% 101.23/101.60 substitution1:
% 101.23/101.60 X := X
% 101.23/101.60 Y := Y
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 subsumption: (7003) {G9,W11,D5,L1,V2,M1} R(6984,46) { ! convergent_lines(
% 101.23/101.60 orthogonal_through_point( X, Y ), orthogonal_through_point( X,
% 101.23/101.60 intersection_point( X, orthogonal_through_point( X, Y ) ) ) ) }.
% 101.23/101.60 parent0: (12060) {G3,W11,D5,L1,V2,M1} { ! convergent_lines(
% 101.23/101.60 orthogonal_through_point( X, Y ), orthogonal_through_point( X,
% 101.23/101.60 intersection_point( X, orthogonal_through_point( X, Y ) ) ) ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := X
% 101.23/101.60 Y := Y
% 101.23/101.60 end
% 101.23/101.60 permutation0:
% 101.23/101.60 0 ==> 0
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 resolution: (12062) {G2,W16,D5,L2,V3,M2} { ! convergent_lines(
% 101.23/101.60 orthogonal_through_point( X, Y ), orthogonal_through_point( X,
% 101.23/101.60 intersection_point( Z, orthogonal_through_point( X, Y ) ) ) ), !
% 101.23/101.60 convergent_lines( orthogonal_through_point( X, Y ), Z ) }.
% 101.23/101.60 parent0[1]: (6984) {G8,W16,D5,L2,V3,M2} R(6192,6346) { ! convergent_lines(
% 101.23/101.60 orthogonal_through_point( Y, Z ), orthogonal_through_point( Y,
% 101.23/101.60 intersection_point( X, orthogonal_through_point( Y, Z ) ) ) ), !
% 101.23/101.60 convergent_lines( X, orthogonal_through_point( Y, Z ) ) }.
% 101.23/101.60 parent1[1]: (43) {G1,W6,D2,L2,V2,M2} R(5,2) { ! convergent_lines( Y, X ),
% 101.23/101.60 convergent_lines( X, Y ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := Z
% 101.23/101.60 Y := X
% 101.23/101.60 Z := Y
% 101.23/101.60 end
% 101.23/101.60 substitution1:
% 101.23/101.60 X := Z
% 101.23/101.60 Y := orthogonal_through_point( X, Y )
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 subsumption: (7004) {G9,W16,D5,L2,V3,M2} R(6984,43) { ! convergent_lines(
% 101.23/101.60 orthogonal_through_point( X, Y ), Z ), ! convergent_lines(
% 101.23/101.60 orthogonal_through_point( X, Y ), orthogonal_through_point( X,
% 101.23/101.60 intersection_point( Z, orthogonal_through_point( X, Y ) ) ) ) }.
% 101.23/101.60 parent0: (12062) {G2,W16,D5,L2,V3,M2} { ! convergent_lines(
% 101.23/101.60 orthogonal_through_point( X, Y ), orthogonal_through_point( X,
% 101.23/101.60 intersection_point( Z, orthogonal_through_point( X, Y ) ) ) ), !
% 101.23/101.60 convergent_lines( orthogonal_through_point( X, Y ), Z ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := X
% 101.23/101.60 Y := Y
% 101.23/101.60 Z := Z
% 101.23/101.60 end
% 101.23/101.60 permutation0:
% 101.23/101.60 0 ==> 1
% 101.23/101.60 1 ==> 0
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 resolution: (12063) {G5,W15,D6,L1,V0,M1} { convergent_lines(
% 101.23/101.60 orthogonal_through_point( orthogonal_through_point( skol2, skol1 ),
% 101.23/101.60 intersection_point( orthogonal_through_point( skol2, skol1 ),
% 101.23/101.60 orthogonal_through_point( orthogonal_through_point( skol2, skol1 ), skol1
% 101.23/101.60 ) ) ), skol2 ) }.
% 101.23/101.60 parent0[0]: (7003) {G9,W11,D5,L1,V2,M1} R(6984,46) { ! convergent_lines(
% 101.23/101.60 orthogonal_through_point( X, Y ), orthogonal_through_point( X,
% 101.23/101.60 intersection_point( X, orthogonal_through_point( X, Y ) ) ) ) }.
% 101.23/101.60 parent1[1]: (4979) {G4,W10,D4,L2,V1,M2} R(4893,151) { convergent_lines( X,
% 101.23/101.60 skol2 ), convergent_lines( orthogonal_through_point(
% 101.23/101.60 orthogonal_through_point( skol2, skol1 ), skol1 ), X ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := orthogonal_through_point( skol2, skol1 )
% 101.23/101.60 Y := skol1
% 101.23/101.60 end
% 101.23/101.60 substitution1:
% 101.23/101.60 X := orthogonal_through_point( orthogonal_through_point( skol2, skol1 )
% 101.23/101.60 , intersection_point( orthogonal_through_point( skol2, skol1 ),
% 101.23/101.60 orthogonal_through_point( orthogonal_through_point( skol2, skol1 ), skol1
% 101.23/101.60 ) ) )
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 subsumption: (7036) {G10,W15,D6,L1,V0,M1} R(7003,4979) { convergent_lines(
% 101.23/101.60 orthogonal_through_point( orthogonal_through_point( skol2, skol1 ),
% 101.23/101.60 intersection_point( orthogonal_through_point( skol2, skol1 ),
% 101.23/101.60 orthogonal_through_point( orthogonal_through_point( skol2, skol1 ), skol1
% 101.23/101.60 ) ) ), skol2 ) }.
% 101.23/101.60 parent0: (12063) {G5,W15,D6,L1,V0,M1} { convergent_lines(
% 101.23/101.60 orthogonal_through_point( orthogonal_through_point( skol2, skol1 ),
% 101.23/101.60 intersection_point( orthogonal_through_point( skol2, skol1 ),
% 101.23/101.60 orthogonal_through_point( orthogonal_through_point( skol2, skol1 ), skol1
% 101.23/101.60 ) ) ), skol2 ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 end
% 101.23/101.60 permutation0:
% 101.23/101.60 0 ==> 0
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 resolution: (12065) {G1,W10,D4,L2,V3,M2} { ! distinct_lines(
% 101.23/101.60 orthogonal_through_point( orthogonal_through_point( Y, Z ), X ), Y ),
% 101.23/101.60 apart_point_and_line( X, Y ) }.
% 101.23/101.60 parent0[0]: (24) {G0,W5,D3,L1,V2,M1} I { ! apart_point_and_line( X,
% 101.23/101.60 orthogonal_through_point( Y, X ) ) }.
% 101.23/101.60 parent1[2]: (4484) {G8,W17,D4,L3,V4,M2} R(300,2981) { ! distinct_lines(
% 101.23/101.60 orthogonal_through_point( orthogonal_through_point( X, Y ), Z ), X ),
% 101.23/101.60 apart_point_and_line( T, X ), apart_point_and_line( T,
% 101.23/101.60 orthogonal_through_point( orthogonal_through_point( X, Y ), Z ) ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := X
% 101.23/101.60 Y := orthogonal_through_point( Y, Z )
% 101.23/101.60 end
% 101.23/101.60 substitution1:
% 101.23/101.60 X := Y
% 101.23/101.60 Y := Z
% 101.23/101.60 Z := X
% 101.23/101.60 T := X
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 subsumption: (7555) {G9,W10,D4,L2,V3,M1} R(4484,24) { ! distinct_lines(
% 101.23/101.60 orthogonal_through_point( orthogonal_through_point( X, Y ), Z ), X ),
% 101.23/101.60 apart_point_and_line( Z, X ) }.
% 101.23/101.60 parent0: (12065) {G1,W10,D4,L2,V3,M2} { ! distinct_lines(
% 101.23/101.60 orthogonal_through_point( orthogonal_through_point( Y, Z ), X ), Y ),
% 101.23/101.60 apart_point_and_line( X, Y ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := Z
% 101.23/101.60 Y := X
% 101.23/101.60 Z := Y
% 101.23/101.60 end
% 101.23/101.60 permutation0:
% 101.23/101.60 0 ==> 0
% 101.23/101.60 1 ==> 1
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 resolution: (12067) {G5,W12,D4,L2,V4,M2} { distinct_lines(
% 101.23/101.60 orthogonal_through_point( X, Y ), Z ), ! distinct_lines(
% 101.23/101.60 orthogonal_through_point( orthogonal_through_point( Z, T ), Y ), Z ) }.
% 101.23/101.60 parent0[1]: (1828) {G4,W8,D3,L2,V3,M1} F(1826);r(34) { distinct_lines(
% 101.23/101.60 orthogonal_through_point( Y, Z ), X ), ! apart_point_and_line( Z, X ) }.
% 101.23/101.60 parent1[1]: (7555) {G9,W10,D4,L2,V3,M1} R(4484,24) { ! distinct_lines(
% 101.23/101.60 orthogonal_through_point( orthogonal_through_point( X, Y ), Z ), X ),
% 101.23/101.60 apart_point_and_line( Z, X ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := Z
% 101.23/101.60 Y := X
% 101.23/101.60 Z := Y
% 101.23/101.60 end
% 101.23/101.60 substitution1:
% 101.23/101.60 X := Z
% 101.23/101.60 Y := T
% 101.23/101.60 Z := Y
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 subsumption: (7603) {G10,W12,D4,L2,V4,M2} R(7555,1828) { distinct_lines(
% 101.23/101.60 orthogonal_through_point( T, Z ), X ), ! distinct_lines(
% 101.23/101.60 orthogonal_through_point( orthogonal_through_point( X, Y ), Z ), X ) }.
% 101.23/101.60 parent0: (12067) {G5,W12,D4,L2,V4,M2} { distinct_lines(
% 101.23/101.60 orthogonal_through_point( X, Y ), Z ), ! distinct_lines(
% 101.23/101.60 orthogonal_through_point( orthogonal_through_point( Z, T ), Y ), Z ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := T
% 101.23/101.60 Y := Z
% 101.23/101.60 Z := X
% 101.23/101.60 T := Y
% 101.23/101.60 end
% 101.23/101.60 permutation0:
% 101.23/101.60 0 ==> 0
% 101.23/101.60 1 ==> 1
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 resolution: (12068) {G3,W12,D4,L2,V3,M2} { ! convergent_lines( X, Y ), !
% 101.23/101.60 distinct_lines( orthogonal_through_point( orthogonal_through_point( X, Z
% 101.23/101.60 ), intersection_point( X, Y ) ), X ) }.
% 101.23/101.60 parent0[1]: (175) {G2,W8,D3,L2,V2,M1} F(168);r(0) { ! convergent_lines( X,
% 101.23/101.60 Y ), ! apart_point_and_line( intersection_point( X, Y ), X ) }.
% 101.23/101.60 parent1[1]: (7555) {G9,W10,D4,L2,V3,M1} R(4484,24) { ! distinct_lines(
% 101.23/101.60 orthogonal_through_point( orthogonal_through_point( X, Y ), Z ), X ),
% 101.23/101.60 apart_point_and_line( Z, X ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := X
% 101.23/101.60 Y := Y
% 101.23/101.60 end
% 101.23/101.60 substitution1:
% 101.23/101.60 X := X
% 101.23/101.60 Y := Z
% 101.23/101.60 Z := intersection_point( X, Y )
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 subsumption: (7607) {G10,W12,D4,L2,V3,M1} R(7555,175) { ! convergent_lines
% 101.23/101.60 ( X, Z ), ! distinct_lines( orthogonal_through_point(
% 101.23/101.60 orthogonal_through_point( X, Y ), intersection_point( X, Z ) ), X ) }.
% 101.23/101.60 parent0: (12068) {G3,W12,D4,L2,V3,M2} { ! convergent_lines( X, Y ), !
% 101.23/101.60 distinct_lines( orthogonal_through_point( orthogonal_through_point( X, Z
% 101.23/101.60 ), intersection_point( X, Y ) ), X ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := X
% 101.23/101.60 Y := Z
% 101.23/101.60 Z := Y
% 101.23/101.60 end
% 101.23/101.60 permutation0:
% 101.23/101.60 0 ==> 0
% 101.23/101.60 1 ==> 1
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 resolution: (12069) {G1,W12,D4,L2,V4,M2} { distinct_lines(
% 101.23/101.60 orthogonal_through_point( X, Y ), Z ), ! convergent_lines(
% 101.23/101.60 orthogonal_through_point( orthogonal_through_point( Z, T ), Y ), Z ) }.
% 101.23/101.60 parent0[1]: (7603) {G10,W12,D4,L2,V4,M2} R(7555,1828) { distinct_lines(
% 101.23/101.60 orthogonal_through_point( T, Z ), X ), ! distinct_lines(
% 101.23/101.60 orthogonal_through_point( orthogonal_through_point( X, Y ), Z ), X ) }.
% 101.23/101.60 parent1[1]: (13) {G0,W6,D2,L2,V2,M1} I { ! convergent_lines( X, Y ),
% 101.23/101.60 distinct_lines( X, Y ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := Z
% 101.23/101.60 Y := T
% 101.23/101.60 Z := Y
% 101.23/101.60 T := X
% 101.23/101.60 end
% 101.23/101.60 substitution1:
% 101.23/101.60 X := orthogonal_through_point( orthogonal_through_point( Z, T ), Y )
% 101.23/101.60 Y := Z
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 subsumption: (9450) {G11,W12,D4,L2,V4,M1} R(7603,13) { ! convergent_lines(
% 101.23/101.60 orthogonal_through_point( orthogonal_through_point( Z, T ), Y ), Z ),
% 101.23/101.60 distinct_lines( orthogonal_through_point( X, Y ), Z ) }.
% 101.23/101.60 parent0: (12069) {G1,W12,D4,L2,V4,M2} { distinct_lines(
% 101.23/101.60 orthogonal_through_point( X, Y ), Z ), ! convergent_lines(
% 101.23/101.60 orthogonal_through_point( orthogonal_through_point( Z, T ), Y ), Z ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := X
% 101.23/101.60 Y := Y
% 101.23/101.60 Z := Z
% 101.23/101.60 T := T
% 101.23/101.60 end
% 101.23/101.60 permutation0:
% 101.23/101.60 0 ==> 1
% 101.23/101.60 1 ==> 0
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 resolution: (12070) {G11,W12,D4,L2,V3,M2} { ! convergent_lines( X, Y ), !
% 101.23/101.60 convergent_lines( orthogonal_through_point( orthogonal_through_point( X,
% 101.23/101.60 T ), intersection_point( X, Y ) ), X ) }.
% 101.23/101.60 parent0[1]: (7607) {G10,W12,D4,L2,V3,M1} R(7555,175) { ! convergent_lines(
% 101.23/101.60 X, Z ), ! distinct_lines( orthogonal_through_point(
% 101.23/101.60 orthogonal_through_point( X, Y ), intersection_point( X, Z ) ), X ) }.
% 101.23/101.60 parent1[1]: (9450) {G11,W12,D4,L2,V4,M1} R(7603,13) { ! convergent_lines(
% 101.23/101.60 orthogonal_through_point( orthogonal_through_point( Z, T ), Y ), Z ),
% 101.23/101.60 distinct_lines( orthogonal_through_point( X, Y ), Z ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := X
% 101.23/101.60 Y := Z
% 101.23/101.60 Z := Y
% 101.23/101.60 end
% 101.23/101.60 substitution1:
% 101.23/101.60 X := orthogonal_through_point( X, Z )
% 101.23/101.60 Y := intersection_point( X, Y )
% 101.23/101.60 Z := X
% 101.23/101.60 T := T
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 subsumption: (11051) {G12,W12,D4,L2,V3,M2} R(7607,9450) { !
% 101.23/101.60 convergent_lines( orthogonal_through_point( orthogonal_through_point( X,
% 101.23/101.60 Z ), intersection_point( X, Y ) ), X ), ! convergent_lines( X, Y ) }.
% 101.23/101.60 parent0: (12070) {G11,W12,D4,L2,V3,M2} { ! convergent_lines( X, Y ), !
% 101.23/101.60 convergent_lines( orthogonal_through_point( orthogonal_through_point( X,
% 101.23/101.60 T ), intersection_point( X, Y ) ), X ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := X
% 101.23/101.60 Y := Y
% 101.23/101.60 Z := T
% 101.23/101.60 T := Z
% 101.23/101.60 end
% 101.23/101.60 permutation0:
% 101.23/101.60 0 ==> 1
% 101.23/101.60 1 ==> 0
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 resolution: (12072) {G2,W12,D4,L2,V3,M2} { ! convergent_lines(
% 101.23/101.60 orthogonal_through_point( orthogonal_through_point( X, Y ),
% 101.23/101.60 intersection_point( X, Z ) ), X ), ! convergent_lines( Z, X ) }.
% 101.23/101.60 parent0[1]: (11051) {G12,W12,D4,L2,V3,M2} R(7607,9450) { ! convergent_lines
% 101.23/101.60 ( orthogonal_through_point( orthogonal_through_point( X, Z ),
% 101.23/101.60 intersection_point( X, Y ) ), X ), ! convergent_lines( X, Y ) }.
% 101.23/101.60 parent1[1]: (43) {G1,W6,D2,L2,V2,M2} R(5,2) { ! convergent_lines( Y, X ),
% 101.23/101.60 convergent_lines( X, Y ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := X
% 101.23/101.60 Y := Z
% 101.23/101.60 Z := Y
% 101.23/101.60 end
% 101.23/101.60 substitution1:
% 101.23/101.60 X := X
% 101.23/101.60 Y := Z
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 subsumption: (11398) {G13,W12,D4,L2,V3,M2} R(11051,43) { ! convergent_lines
% 101.23/101.60 ( Z, X ), ! convergent_lines( orthogonal_through_point(
% 101.23/101.60 orthogonal_through_point( X, Y ), intersection_point( X, Z ) ), X ) }.
% 101.23/101.60 parent0: (12072) {G2,W12,D4,L2,V3,M2} { ! convergent_lines(
% 101.23/101.60 orthogonal_through_point( orthogonal_through_point( X, Y ),
% 101.23/101.60 intersection_point( X, Z ) ), X ), ! convergent_lines( Z, X ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := X
% 101.23/101.60 Y := Y
% 101.23/101.60 Z := Z
% 101.23/101.60 end
% 101.23/101.60 permutation0:
% 101.23/101.60 0 ==> 1
% 101.23/101.60 1 ==> 0
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 resolution: (12076) {G3,W15,D4,L3,V4,M3} { ! convergent_lines( X, Y ),
% 101.23/101.60 convergent_lines( T, orthogonal_through_point( orthogonal_through_point(
% 101.23/101.60 Y, Z ), intersection_point( Y, X ) ) ), ! convergent_lines( T, Y ) }.
% 101.23/101.60 parent0[1]: (11398) {G13,W12,D4,L2,V3,M2} R(11051,43) { ! convergent_lines
% 101.23/101.60 ( Z, X ), ! convergent_lines( orthogonal_through_point(
% 101.23/101.60 orthogonal_through_point( X, Y ), intersection_point( X, Z ) ), X ) }.
% 101.23/101.60 parent1[2]: (45) {G2,W9,D2,L3,V3,M3} R(43,5) { convergent_lines( Z, X ), !
% 101.23/101.60 convergent_lines( Z, Y ), convergent_lines( X, Y ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := Y
% 101.23/101.60 Y := Z
% 101.23/101.60 Z := X
% 101.23/101.60 end
% 101.23/101.60 substitution1:
% 101.23/101.60 X := orthogonal_through_point( orthogonal_through_point( Y, Z ),
% 101.23/101.60 intersection_point( Y, X ) )
% 101.23/101.60 Y := Y
% 101.23/101.60 Z := T
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 subsumption: (11629) {G14,W15,D4,L3,V4,M3} R(11398,45) { convergent_lines(
% 101.23/101.60 Z, orthogonal_through_point( orthogonal_through_point( Y, T ),
% 101.23/101.60 intersection_point( Y, X ) ) ), ! convergent_lines( Z, Y ), !
% 101.23/101.60 convergent_lines( X, Y ) }.
% 101.23/101.60 parent0: (12076) {G3,W15,D4,L3,V4,M3} { ! convergent_lines( X, Y ),
% 101.23/101.60 convergent_lines( T, orthogonal_through_point( orthogonal_through_point(
% 101.23/101.60 Y, Z ), intersection_point( Y, X ) ) ), ! convergent_lines( T, Y ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := X
% 101.23/101.60 Y := Y
% 101.23/101.60 Z := T
% 101.23/101.60 T := Z
% 101.23/101.60 end
% 101.23/101.60 permutation0:
% 101.23/101.60 0 ==> 2
% 101.23/101.60 1 ==> 0
% 101.23/101.60 2 ==> 1
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 factor: (12079) {G14,W12,D4,L2,V3,M2} { convergent_lines( X,
% 101.23/101.60 orthogonal_through_point( orthogonal_through_point( Y, Z ),
% 101.23/101.60 intersection_point( Y, X ) ) ), ! convergent_lines( X, Y ) }.
% 101.23/101.60 parent0[1, 2]: (11629) {G14,W15,D4,L3,V4,M3} R(11398,45) { convergent_lines
% 101.23/101.60 ( Z, orthogonal_through_point( orthogonal_through_point( Y, T ),
% 101.23/101.60 intersection_point( Y, X ) ) ), ! convergent_lines( Z, Y ), !
% 101.23/101.60 convergent_lines( X, Y ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := X
% 101.23/101.60 Y := Y
% 101.23/101.60 Z := X
% 101.23/101.60 T := Z
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 subsumption: (11646) {G15,W12,D4,L2,V3,M2} F(11629) { ! convergent_lines( X
% 101.23/101.60 , Y ), convergent_lines( X, orthogonal_through_point(
% 101.23/101.60 orthogonal_through_point( Y, Z ), intersection_point( Y, X ) ) ) }.
% 101.23/101.60 parent0: (12079) {G14,W12,D4,L2,V3,M2} { convergent_lines( X,
% 101.23/101.60 orthogonal_through_point( orthogonal_through_point( Y, Z ),
% 101.23/101.60 intersection_point( Y, X ) ) ), ! convergent_lines( X, Y ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := X
% 101.23/101.60 Y := Y
% 101.23/101.60 Z := Z
% 101.23/101.60 end
% 101.23/101.60 permutation0:
% 101.23/101.60 0 ==> 1
% 101.23/101.60 1 ==> 0
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 resolution: (12081) {G10,W14,D4,L2,V3,M2} { ! convergent_lines(
% 101.23/101.60 orthogonal_through_point( orthogonal_through_point( X, Y ), Z ), X ), !
% 101.23/101.60 convergent_lines( orthogonal_through_point( orthogonal_through_point( X,
% 101.23/101.60 Y ), Z ), X ) }.
% 101.23/101.60 parent0[1]: (7004) {G9,W16,D5,L2,V3,M2} R(6984,43) { ! convergent_lines(
% 101.23/101.60 orthogonal_through_point( X, Y ), Z ), ! convergent_lines(
% 101.23/101.60 orthogonal_through_point( X, Y ), orthogonal_through_point( X,
% 101.23/101.60 intersection_point( Z, orthogonal_through_point( X, Y ) ) ) ) }.
% 101.23/101.60 parent1[1]: (11646) {G15,W12,D4,L2,V3,M2} F(11629) { ! convergent_lines( X
% 101.23/101.60 , Y ), convergent_lines( X, orthogonal_through_point(
% 101.23/101.60 orthogonal_through_point( Y, Z ), intersection_point( Y, X ) ) ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := orthogonal_through_point( X, Y )
% 101.23/101.60 Y := Z
% 101.23/101.60 Z := X
% 101.23/101.60 end
% 101.23/101.60 substitution1:
% 101.23/101.60 X := orthogonal_through_point( orthogonal_through_point( X, Y ), Z )
% 101.23/101.60 Y := X
% 101.23/101.60 Z := Y
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 factor: (12082) {G10,W7,D4,L1,V3,M1} { ! convergent_lines(
% 101.23/101.60 orthogonal_through_point( orthogonal_through_point( X, Y ), Z ), X ) }.
% 101.23/101.60 parent0[0, 1]: (12081) {G10,W14,D4,L2,V3,M2} { ! convergent_lines(
% 101.23/101.60 orthogonal_through_point( orthogonal_through_point( X, Y ), Z ), X ), !
% 101.23/101.60 convergent_lines( orthogonal_through_point( orthogonal_through_point( X,
% 101.23/101.60 Y ), Z ), X ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := X
% 101.23/101.60 Y := Y
% 101.23/101.60 Z := Z
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 subsumption: (11653) {G16,W7,D4,L1,V3,M1} R(11646,7004);f { !
% 101.23/101.60 convergent_lines( orthogonal_through_point( orthogonal_through_point( X,
% 101.23/101.60 Y ), Z ), X ) }.
% 101.23/101.60 parent0: (12082) {G10,W7,D4,L1,V3,M1} { ! convergent_lines(
% 101.23/101.60 orthogonal_through_point( orthogonal_through_point( X, Y ), Z ), X ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := X
% 101.23/101.60 Y := Y
% 101.23/101.60 Z := Z
% 101.23/101.60 end
% 101.23/101.60 permutation0:
% 101.23/101.60 0 ==> 0
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 resolution: (12083) {G11,W0,D0,L0,V0,M0} { }.
% 101.23/101.60 parent0[0]: (11653) {G16,W7,D4,L1,V3,M1} R(11646,7004);f { !
% 101.23/101.60 convergent_lines( orthogonal_through_point( orthogonal_through_point( X,
% 101.23/101.60 Y ), Z ), X ) }.
% 101.23/101.60 parent1[0]: (7036) {G10,W15,D6,L1,V0,M1} R(7003,4979) { convergent_lines(
% 101.23/101.60 orthogonal_through_point( orthogonal_through_point( skol2, skol1 ),
% 101.23/101.60 intersection_point( orthogonal_through_point( skol2, skol1 ),
% 101.23/101.60 orthogonal_through_point( orthogonal_through_point( skol2, skol1 ), skol1
% 101.23/101.60 ) ) ), skol2 ) }.
% 101.23/101.60 substitution0:
% 101.23/101.60 X := skol2
% 101.23/101.60 Y := skol1
% 101.23/101.60 Z := intersection_point( orthogonal_through_point( skol2, skol1 ),
% 101.23/101.60 orthogonal_through_point( orthogonal_through_point( skol2, skol1 ), skol1
% 101.23/101.60 ) )
% 101.23/101.60 end
% 101.23/101.60 substitution1:
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 subsumption: (11790) {G17,W0,D0,L0,V0,M0} S(7036);r(11653) { }.
% 101.23/101.60 parent0: (12083) {G11,W0,D0,L0,V0,M0} { }.
% 101.23/101.60 substitution0:
% 101.23/101.60 end
% 101.23/101.60 permutation0:
% 101.23/101.60 end
% 101.23/101.60
% 101.23/101.60 Proof check complete!
% 101.23/101.60
% 101.23/101.60 Memory use:
% 101.23/101.60
% 101.23/101.60 space for terms: 194947
% 101.23/101.60 space for clauses: 516449
% 101.23/101.60
% 101.23/101.60
% 101.23/101.60 clauses generated: 15415738
% 101.23/101.60 clauses kept: 11791
% 101.23/101.60 clauses selected: 6718
% 101.23/101.60 clauses deleted: 383
% 101.23/101.60 clauses inuse deleted: 39
% 101.23/101.60
% 101.23/101.60 subsentry: 75372800
% 101.23/101.60 literals s-matched: 22478020
% 101.23/101.60 literals matched: 22475679
% 101.23/101.60 full subsumption: 14771777
% 101.23/101.60
% 101.23/101.60 checksum: 2076935950
% 101.23/101.60
% 101.23/101.60
% 101.23/101.60 Bliksem ended
%------------------------------------------------------------------------------