?- time(run_all(-1)). ============================================================================== Experiment sect(3)-1 ============================================================================== Relates to proof in Fig. 2 and Examples 2,3,6,8 for axiom Syll-Simp ------------------------------------------------------------------------------ % Installing axioms: [1-(((A=>B)=>C)=>(B=>C))] The D-term: d(d(1,1),d(d(1,d(1,1)),d(1,d(1,1)))) Measures - tree size: 7, height: 4, compacted size: 4 Compound Subterms: [d(1, 1), d(1, d(1, 1)), d(d(1, 1), d(d(1, d(1, 1)), d(1, d(1, 1)))), d(d(1, d(1, 1)), d(1, d(1, 1)))] The D-term in factor notation (as in Fig. 2c and Example 8): 2 = d(1, 1) 3 = d(1, 2) 4 = d(2, d(3, 3)) The proven formula in different notations: Łukasiewicz's notation: CpCqCrCsCtCus Term notation with i/2: i(P,i(Q,i(R,i(S,i(T,i(U,S)))))) CDTools notation: P=>(Q=>(R=>(S=>(T=>(U=>S))))) ============================================================================== Experiment sect(3)-2 ============================================================================== Relates to Table 1 ------------------------------------------------------------------------------ % Installing axioms: [1-A] Number of D-terms of tree size 0: 1 Number of D-terms of tree size 1: 1 Number of D-terms of tree size 2: 2 Number of D-terms of tree size 3: 5 Number of D-terms of tree size 4: 14 Number of D-terms of tree size 5: 42 Number of D-terms of height 0: 1 Number of D-terms of height 1: 1 Number of D-terms of height 2: 3 Number of D-terms of height 3: 21 Number of D-terms of height 4: 651 Number of D-terms of height 5: 457,653 Number of D-terms of compacted size 0: 1 Number of D-terms of compacted size 1: 1 Number of D-terms of compacted size 2: 3 Number of D-terms of compacted size 3: 15 Number of D-terms of compacted size 4: 111 Number of D-terms of compacted size 5: 1,119 ============================================================================== Experiment sect(3)-3 ============================================================================== Relates to Example 25 ------------------------------------------------------------------------------ % Installing axioms: [1-(A=>(B=>A))] MGT of d(1,1): P=>(Q=>(R=>Q)) IPT of the occurrence of d(1,1) in d(d(1,1),1): (P=>(Q=>P))=>(R=>(S=>R)) ============================================================================== Experiment sect(4)-1 ============================================================================== Relates to text following Definition 30 and Examples 32, 34 ------------------------------------------------------------------------------ d(d(d(1,1),1),1) >_c d(1,d(1,1)) 1 >=_c d(1,1) d(1,d(1,d(1,1))) >=_c d(d(1,d(1,1)),1) d(1,d(1,d(1,1))) >_c d(d(1,1),1) d(1,d(1,d(1,d(1,1)))) >_c d(d(1,d(1,1)),d(1,d(1,1))) d(1,d(2,d(3,3))) >_c d(4,d(3,3)) d(1,d(1,d(1,d(1,1)))) -- d(1,d(d(1,1),1)) d(1,d(2,d(3,3))) -- d(4,d(5,5)) ============================================================================== Experiment sect(4)-2 ============================================================================== Relates to Examples 36, 37 ------------------------------------------------------------------------------ sc size of d(d(d(1,1),d(1,1)),d(d(1,1),1)): 9 c-sizes: 8 7, sc-sizes: 27 28 ============================================================================== Experiment sect(4)-3 ============================================================================== Relates to Example 39 ------------------------------------------------------------------------------ Compacted sizes: 4 4 SC sizes: 10 9 ============================================================================== Experiment sect(4)-4 ============================================================================== Relates to Example 40 ------------------------------------------------------------------------------ Compacted sizes: 5 4 Compacted sizes: 5 6 ============================================================================== Experiment sect(4)-5 ============================================================================== Relates to Proposition 41 ------------------------------------------------------------------------------ Checking D-terms of tree size 1 Checking D-terms of tree size 2 Checking D-terms of tree size 3 Checking D-terms of tree size 4 Checking D-terms of tree size 5 Found no counterexample for Prop. 41 ============================================================================== Experiment sect(4)-6 ============================================================================== Relates to Examples 48, 49 ------------------------------------------------------------------------------ % Installing axioms: [1-(((A=>B)=>C)=>(B=>C))] Axiom: syll_simp D-term: d(d(d(1,1),1),1) Regularity wrt. IS: no; MS: no; S: no % Installing axioms: [1-(((A=>B)=>C)=>((C=>A)=>(D=>A)))] Axiom: luk D-term: d(d(d(d(1,d(1,1)),1),1),d(1,1)) Regularity wrt. IS: yes; MS: yes; S: no ============================================================================== Experiment sect(5)-1 ============================================================================== Relates to Section 5.4.1 DC, DT, DH: Comapcted Size, Tree Size and Height ------------------------------------------------------------------------------ % Installing axioms: [1-(((A=>B)=>C)=>((C=>A)=>(D=>A)))] -------------------------------------------------------------------- Dimensions of the subproof of Syll -------------------------------------------------------------------- DC (compacted size) Mer: 31 Łuk: 32 DT (tree size) Mer: 491 Łuk: 435 DH (height) Mer: 29 Łuk: 29 -------------------------------------------------------------------- Dimensions of the subproof of Syll - before n-simplification -------------------------------------------------------------------- Before n-simplification DC (compacted size) Mer: 31 Łuk: 32 DT (tree size) Mer: 491 Łuk: 563 DH (height) Mer: 29 Łuk: 29 -------------------------------------------------------------------- Dimensions of the overall proof -------------------------------------------------------------------- Overall compacted size Mer: 33 Łuk: 34 Overall tree size Mer: 669 Łuk: 585 Overall height Mer: 29 Łuk: 29 -------------------------------------------------------------------- Dimensions of the overall proof - before n-simplification -------------------------------------------------------------------- Overall compacted size Mer: 33 Łuk: 34 Overall tree size Mer: 669 Łuk: 751 Overall height Mer: 29 Łuk: 29 ============================================================================== Experiment sect(5)-2 ============================================================================== Relates to Section 5.4.5 DP: Is Prime ------------------------------------------------------------------------------ % Installing axioms: [1-A] Number of prime dterms at level 0: 1 Number of prime dterms at level 1: 1 Number of prime dterms at level 2: 2 Number of prime dterms at level 3: 4 Number of prime dterms at level 4: 8 Number of prime dterms at level 5: 16 Number of prime dterms at level 6: 32 Number of prime dterms at level 7: 64 % Installing axioms: [1-(((A=>B)=>C)=>((C=>A)=>(D=>A)))] Trying to prove ((p=>q)=>(r=>s))=>((p=>s)=>(r=>s)) from luk by prime level enumeration Found prime proof at level 17: d(d(d(d(1,d(1,d(1,d(1,d(d(d(d(1,d(d(d(1,d(1,d(1,d(1,1)))),1),1)),1),1),1))))),1),1),1) ============================================================================== Experiment sect(5)-3 ============================================================================== Relates to Section 5.6.1 ------------------------------------------------------------------------------ % Installing axioms: [1-(((A=>B)=>C)=>((C=>A)=>(D=>A)))] Proof of simp in Mer - tree size: 19 compacted size: 10 Proof of simp in Łuk: - tree size: 19 compacted size: 10 Found proof of simp with min. tree size 7: d(d(d(1,1),d(d(d(1,d(1,1)),1),1)),1) Found proof of simp with min. compacted size 6: d(d(d(1,1),d(d(d(1,d(1,1)),1),d(d(1,d(1,1)),1))),d(d(1,1),d(d(d(1,d(1,1)),1),d(d(1,d(1,1)),1)))) Proof of peirce in Mer - tree size: 159 compacted size: 26 Proof of peirce in Łuk: - tree size: 131 compacted size: 29 Found proof of peirce with min. tree size 15: d(d(d(1,d(d(d(1,d(1,d(d(d(1,d(1,1)),1),1))),1),1)),d(d(d(1,d(1,1)),1),1)),1) ============================================================================== Experiment sect(5)-4 ============================================================================== Relates to Section 5.6.1 ------------------------------------------------------------------------------ Skipping experiment due to failed requirement: longtime ============================================================================== Experiment sect(6)-1 ============================================================================== Relates to demo of Prover9 in PIE: Syll and Peirce from axiom Łukasiewicz ------------------------------------------------------------------------------ Proving problem LCL082-1 with Prover9 % Reading TPTP file % Loading tptp file: /home/ch/space/tptp/TPTP-v8.1.2/Problems/LCL/LCL082-1.p % Reading TPTP file % Loading tptp file: /home/ch/space/tptp/TPTP-v8.1.2/Problems/LCL/LCL082-1.p % Installing axioms: [1-(((A=>B)=>C)=>((C=>A)=>(D=>A)))] % Reading TPTP file % Loading tptp file: /home/ch/space/tptp/TPTP-v8.1.2/Problems/LCL/LCL082-1.p % Reading TPTP file % Loading tptp file: /home/ch/space/tptp/TPTP-v8.1.2/Problems/LCL/LCL082-1.p % Calling prover9 /tmp/swipl_1284866_2.output 2>>/tmp/swipl_1284866_3.error % Calling prooftrans xml renumber xml -f /tmp/swipl_1284866_2.output >/tmp/swipl_1284866_5 % Loading proofs from /tmp/swipl_1284866_5 % Initializing prooftrans DTD Proving time: 0.00 s Found proof: d(d(d(1,1),d(1,d(d(d(1,d(1,1)),d(1,d(d(d(1,1),d(1,1)),d(d(1,1),d(1,1))))),d(d(1,d(1,1)),d(1,d(d(d(1,1),d(1,1)),d(d(1,1),d(1,1)))))))),d(d(1,1),d(1,d(d(d(1,d(1,1)),d(1,d(d(d(1,1),d(1,1)),d(d(1,1),d(1,1))))),d(d(1,d(1,1)),d(1,d(d(d(1,1),d(1,1)),d(d(1,1),d(1,1))))))))) Proving problem LCL083-1 with Prover9 % Reading TPTP file % Loading tptp file: /home/ch/space/tptp/TPTP-v8.1.2/Problems/LCL/LCL083-1.p % Reading TPTP file % Loading tptp file: /home/ch/space/tptp/TPTP-v8.1.2/Problems/LCL/LCL083-1.p % Installing axioms: [1-(((A=>B)=>C)=>((C=>A)=>(D=>A)))] % Reading TPTP file % Loading tptp file: /home/ch/space/tptp/TPTP-v8.1.2/Problems/LCL/LCL083-1.p % Reading TPTP file % Loading tptp file: /home/ch/space/tptp/TPTP-v8.1.2/Problems/LCL/LCL083-1.p % Calling prover9 /tmp/swipl_1284866_8.output 2>>/tmp/swipl_1284866_9.error % Calling prooftrans xml renumber xml -f /tmp/swipl_1284866_8.output >/tmp/swipl_1284866_11 % Loading proofs from /tmp/swipl_1284866_11 Proving time: 0.06 s Found proof: d(d(d(1,d(d(d(1,d(1,d(1,d(d(d(d(1,d(1,1)),d(1,d(d(d(1,1),d(1,1)),d(d(1,1),d(1,1))))),d(d(1,d(1,1)),d(1,d(d(d(1,1),d(1,1)),d(d(1,1),d(1,1)))))),d(1,d(d(d(1,1),d(1,1)),d(d(1,1),d(1,1)))))))),1),d(d(1,d(1,d(1,d(d(d(d(1,d(1,1)),d(1,d(d(d(1,1),d(1,1)),d(d(1,1),d(1,1))))),d(d(1,d(1,1)),d(1,d(d(d(1,1),d(1,1)),d(d(1,1),d(1,1)))))),d(1,d(d(d(1,1),d(1,1)),d(d(1,1),d(1,1)))))))),1))),d(1,d(d(d(d(1,d(1,1)),d(1,d(d(d(1,1),d(1,1)),d(d(1,1),d(1,1))))),d(d(1,d(1,1)),d(1,d(d(d(1,1),d(1,1)),d(d(1,1),d(1,1)))))),d(1,d(d(d(1,1),d(1,1)),d(d(1,1),d(1,1))))))),d(d(1,d(d(d(1,d(1,d(1,d(d(d(d(1,d(1,1)),d(1,d(d(d(1,1),d(1,1)),d(d(1,1),d(1,1))))),d(d(1,d(1,1)),d(1,d(d(d(1,1),d(1,1)),d(d(1,1),d(1,1)))))),d(1,d(d(d(1,1),d(1,1)),d(d(1,1),d(1,1)))))))),1),d(d(1,d(1,d(1,d(d(d(d(1,d(1,1)),d(1,d(d(d(1,1),d(1,1)),d(d(1,1),d(1,1))))),d(d(1,d(1,1)),d(1,d(d(d(1,1),d(1,1)),d(d(1,1),d(1,1)))))),d(1,d(d(d(1,1),d(1,1)),d(d(1,1),d(1,1)))))))),1))),d(1,d(d(d(d(1,d(1,1)),d(1,d(d(d(1,1),d(1,1)),d(d(1,1),d(1,1))))),d(d(1,d(1,1)),d(1,d(d(d(1,1),d(1,1)),d(d(1,1),d(1,1)))))),d(1,d(d(d(1,1),d(1,1)),d(d(1,1),d(1,1)))))))) ============================================================================== Experiment sect(6)-2 ============================================================================== Relates to Section 6.2: Prover9's proofs and reductions ------------------------------------------------------------------------------ ------------------------------------------------------------------------------ Det mode minor_major % Reading TPTP file % Loading tptp file: /home/ch/space/tptp/TPTP-v8.1.2/Problems/LCL/LCL038-1.p % Reading TPTP file % Loading tptp file: /home/ch/space/tptp/TPTP-v8.1.2/Problems/LCL/LCL038-1.p % Installing axioms: [1-(((A=>B)=>C)=>((C=>A)=>(D=>A)))] % Reading TPTP file % Loading tptp file: /home/ch/space/tptp/TPTP-v8.1.2/Problems/LCL/LCL038-1.p % Reading TPTP file % Loading tptp file: /home/ch/space/tptp/TPTP-v8.1.2/Problems/LCL/LCL038-1.p % Calling prover9 /tmp/swipl_1284866_13.output 2>>/tmp/swipl_1284866_14.error % Calling prooftrans xml renumber xml -f /tmp/swipl_1284866_13.output >/tmp/swipl_1284866_16 % Loading proofs from /tmp/swipl_1284866_16 Proving time: 19.54 s ---- (1) Given proof: DC: 94; DT: 304,890; DH: 40; DX: 3,247 FT-Max: 11; FH-Max: 7 Regularity RS: no; RC: no ---- (2) N-simplification of (1): Occurrences of n: 1,708 DC: 83; DT: 8,217; DH: 38; DX: 2,485 FT-Max: 11; FH-Max: 7 Regularity RS: no; RC: no ---- (3) S-reduction of (2): % Progress: 61 S-reduction steps: 61 DC: 80; DT: 7,058; DH: 38; DX: 2,311 FT-Max: 13; FH-Max: 7 Regularity RS: yes; RC: no ---- (4) C-reduction of (2): % Progress: 2 C-reduction steps: 2 DC: 80; DT: 5,746; DH: 36; DX: 2,290 FT-Max: 13; FH-Max: 7 Regularity RS: yes; RC: yes ---- (5) C-reduction of (2): % Progress: 1 C-reduction steps: 1 DC: 80; DT: 5,746; DH: 36; DX: 2,290 FT-Max: 13; FH-Max: 7 Regularity RS: yes; RC: yes ------------------------------------------------------------------------------ Det mode major_minor % Reading TPTP file % Loading tptp file: /home/ch/space/tptp/TPTP-v8.1.2/Problems/LCL/LCL038-1.p % Reading TPTP file % Loading tptp file: /home/ch/space/tptp/TPTP-v8.1.2/Problems/LCL/LCL038-1.p % Installing axioms: [1-(((A=>B)=>C)=>((C=>A)=>(D=>A)))] % Reading TPTP file % Loading tptp file: /home/ch/space/tptp/TPTP-v8.1.2/Problems/LCL/LCL038-1.p % Reading TPTP file % Loading tptp file: /home/ch/space/tptp/TPTP-v8.1.2/Problems/LCL/LCL038-1.p % Calling prover9 /tmp/swipl_1284866_18.output 2>>/tmp/swipl_1284866_19.error % Calling prooftrans xml renumber xml -f /tmp/swipl_1284866_18.output >/tmp/swipl_1284866_21 % Loading proofs from /tmp/swipl_1284866_21 Proving time: 23.01 s ---- (1) Given proof: DC: 93; DT: 216,094; DH: 40; DX: 3,011 FT-Max: 11; FH-Max: 7 Regularity RS: no; RC: no ---- (2) N-simplification of (1): Occurrences of n: 3,700 DC: 91; DT: 18,261; DH: 38; DX: 2,870 FT-Max: 11; FH-Max: 7 Regularity RS: no; RC: no ---- (3) S-reduction of (2): % Progress: 281 S-reduction steps: 281 DC: 88; DT: 12,922; DH: 38; DX: 2,669 FT-Max: 13; FH-Max: 7 Regularity RS: yes; RC: no ---- (4) C-reduction of (2): % Progress: 6 C-reduction steps: 6 DC: 84; DT: 8,200; DH: 36; DX: 2,410 FT-Max: 13; FH-Max: 7 Regularity RS: yes; RC: yes ---- (5) C-reduction of (2): % Progress: 5 C-reduction steps: 5 DC: 84; DT: 8,200; DH: 36; DX: 2,410 FT-Max: 13; FH-Max: 7 Regularity RS: yes; RC: yes ============================================================================== Experiment sect(6)-3 ============================================================================== Relates to Section 6.2, Definition 52 ------------------------------------------------------------------------------ Cardinality of PSP level 0: 1 Cardinality of PSP level 1: 1 Cardinality of PSP level 2: 3 Cardinality of PSP level 3: 15 Cardinality of PSP level 4: 105 Cardinality of PSP level 5: 945 Cardinality of PSP level 6: 10,395 Cardinality of PSP level 7: 135,135 Cardinality of PSP level 8: 2,027,025 ============================================================================== Experiment sect(6)-4 ============================================================================== Relates to finding the short proof of Syll from axiom Łukasiewicz with SGCD ------------------------------------------------------------------------------ % Reading TPTP file % Loading tptp file: /home/ch/space/tptp/TPTP-v8.1.2/Problems/LCL/LCL038-1.p % Reading TPTP file % Loading tptp file: /home/ch/space/tptp/TPTP-v8.1.2/Problems/LCL/LCL038-1.p % Installing axioms: [1-(((A=>B)=>C)=>((C=>A)=>(D=>A)))] % Effective levels test: [lt_fh(7),lt_ft(19),lt_dup,lt_subs] % Pre-level: 0 for 0 % Creating level: 0 % Process news: reg % new_level_solution/3: 1 clauses % level_solution/3: 1 clauses % Pre-level: 1 for 1 % Creating level: 1 % Process news: reg % new_level_solution/3: 1 clauses % level_solution/3: 2 clauses % Pre-level: 2 for 2 % Creating level: 2 % Process news: reg % new_level_solution/3: 2 clauses % level_solution/3: 4 clauses % Pre-level: 3 for 3 % Creating level: 3 % Process news: reg % new_level_solution/3: 7 clauses % level_solution/3: 10 clauses % Pre-level: 4 for 4 % Creating level: 4 % Process news: reg % new_level_solution/3: 15 clauses % level_solution/3: 25 clauses % Pre-level: 5 for 5 % Creating level: 5 % Process news: reg % new_level_solution/3: 35 clauses % level_solution/3: 46 clauses % Pre-level: 6 for 6 % Creating level: 6 % Process news: reg % new_level_solution/3: 35 clauses % level_solution/3: 74 clauses % Pre-level: 7 for 7 % Creating level: 7 % Process news: reg % new_level_solution/3: 66 clauses % level_solution/3: 126 clauses % Pre-level: 8 for 8 % Creating level: 8 % Process news: reg % new_level_solution/3: 91 clauses % level_solution/3: 201 clauses % Pre-level: 9 for 9 % Creating level: 9 % Process news: reg % new_level_solution/3: 94 clauses % level_solution/3: 278 clauses % Pre-level: 10 for 10 % Creating level: 10 % Process news: reg % new_level_solution/3: 91 clauses % level_solution/3: 359 clauses % Pre-level: 11 for 11 % Creating level: 11 % Process news: reg % new_level_solution/3: 91 clauses % level_solution/3: 443 clauses % Pre-level: 12 for 12 % Creating level: 12 % Process news: reg % new_level_solution/3: 80 clauses % level_solution/3: 519 clauses % Pre-level: 13 for 13 % Creating level: 13 % Process news: reg % new_level_solution/3: 101 clauses % level_solution/3: 608 clauses % Pre-level: 14 for 14 % Creating level: 14 % Process news: reg % new_level_solution/3: 116 clauses % level_solution/3: 714 clauses % Pre-level: 15 for 15 % Creating level: 15 % Process news: reg % new_level_solution/3: 142 clauses % level_solution/3: 836 clauses % Pre-level: 16 for 16 % Creating level: 16 % Process news: reg % new_level_solution/3: 117 clauses % level_solution/3: 942 clauses % Pre-level: 17 for 17 % Creating level: 17 % Process news: reg % new_level_solution/3: 160 clauses % level_solution/3: 1,088 clauses % Pre-level: 18 for 18 % Creating level: 18 % Process news: reg % new_level_solution/3: 195 clauses % level_solution/3: 1,271 clauses % Pre-level: 19 for 19 % Creating level: 19 % Process news: reg % new_level_solution/3: 282 clauses % level_solution/3: 1,534 clauses % Pre-level: 20 for 20 % Creating level: 20 % Process news: reg % new_level_solution/3: 470 clauses % level_solution/3: 1,975 clauses % Pre-level: 21 for 21 % Creating level: 21 % Process news: reg % new_level_solution/3: 1,051 clauses % level_solution/3: 2,900 clauses % Pre-level: 22 for 22 Found poroof: d(d(d(d(1,d(d(d(1,d(d(d(d(d(d(1,d(1,d(1,d(1,d(d(d(d(1,d(1,d(1,1))),1),1),1))))),1),1),1),1),d(d(d(d(1,d(1,d(1,d(1,d(d(d(d(1,d(1,d(1,1))),1),1),1))))),1),1),1))),d(1,d(d(d(d(d(d(1,d(1,d(1,d(1,d(d(d(d(1,d(1,d(1,1))),1),1),1))))),1),1),1),1),d(d(d(d(1,d(1,d(1,d(1,d(d(d(d(1,d(1,d(1,1))),1),1),1))))),1),1),1)))),1)),1),1),1) Used time 1.29s Measures - compacted size: 22, tree size: 64, height: 22 ============================================================================== Experiment sect(6)-5 ============================================================================== Relates to combinator compression of the short proof of Syll ------------------------------------------------------------------------------ ------------------------------------------------------------ Compressed proof in factorized D-term notation: 2 = d(d(B, 1), 1) 3 = d(I', 1) 4 = d(d(d(B4, 3), 3), 3) 5 = d(4, d(2, d(2, d(4, d(2, d(3, 1)))))) 6 = d(1, d(d(3, 5), 5)) 7 = d(4, d(1, d(3, d(6, 6)))) ------------------------------------------------------------ Compressed proof in factorized application notation: 2 = B 1 1 3 = I' 1 4 = B4 3 3 3 5 = 4 (2 (2 (4 (2 (3 1))))) 6 = 1 (3 5 5) 7 = 4 (1 (3 (6 6))) % 15,686,773,897 inferences, 852.258 CPU in 894.972 seconds (95% CPU, 18406141 Lips)