Script started on 2024-09-03 05:34:33-07:00 [COMMAND="swipl /home/deb12user/metta-wam/src/canary/metta_interp.pl -- --python=enable -- --debug --html --log ./tests/baseline_compat/hyperon-mettalog_sanity/synth_buffer/synthesize.metta --time=debug --repl --stdin=tty --stdout=tty --stderr=tty" TERM="xterm" TTY="/dev/pts/7" COLUMNS="115" LINES="24"]
; (set_option_value prolog false)
; (set_option_value compat auto)
; (set_option_value compatio true)
; (is_cmd_option execute python --python=enable enable)
; (set_option_value python enable)
; (is_cmd_option execute debug --debug true)
; (set_option_value debug true)
; (is_cmd_option execute html --html true)
; (set_option_value html true)
; (load_metta_file &self ./tests/baseline_compat/hyperon-mettalog_sanity/synth_buffer/synthesize.metta)
; (track_load_into_file /home/deb12user/metta-wam/tests/baseline_compat/hyperon-mettalog_sanity/synth_buffer/synthesize.metta)
; (load_answer_file /home/deb12user/metta-wam/tests/baseline_compat/hyperon-mettalog_sanity/synth_buffer/synthesize.metta.answers /home/deb12user/metta-wam/tests/baseline_compat/hyperon-mettalog_sanity/synth_buffer/synthesize.metta)
; (= 1 "[(: a B), (: cde (Implication (OrLink C D) E)), (: a A), (: abc (Implication (AndLink A B) C)), (: (DisjunctionIntroduction a a) (OrLink B B)), (: (DisjunctionIntroduction a cde) (OrLink B (Implication (OrLink C D) E))), (: (DisjunctionIntroduction a a) (OrLink B A)), (: (DisjunctionIntroduction a abc) (OrLink B (Implication (AndLink A B) C))), (: (DisjunctionIntroduction cde a) (OrLink (Implication (OrLink C D) E) B)), (: (DisjunctionIntroduction cde cde) (OrLink (Implication (OrLink C D) E) (Implication (OrLink C D) E))), (: (DisjunctionIntroduction cde a) (OrLink (Implication (OrLink C D) E) A)), (: (DisjunctionIntroduction cde abc) (OrLink (Implication (OrLink C D) E) (Implication (AndLink A B) C))), (: (DisjunctionIntroduction a a) (OrLink A B)), (: (DisjunctionIntroduction a cde) (OrLink A (Implication (OrLink C D) E))), (: (DisjunctionIntroduction a a) (OrLink A A)), (: (DisjunctionIntroduction a abc) (OrLink A (Implication (AndLink A B) C))), (: (DisjunctionIntroduction abc a) (OrLink (Implication (AndLink A B) C) B)), (: (DisjunctionIntroduction abc cde) (OrLink (Implication (AndLink A B) C) (Implication (OrLink C D) E))), (: (DisjunctionIntroduction abc a) (OrLink (Implication (AndLink A B) C) A)), (: (DisjunctionIntroduction abc abc) (OrLink (Implication (AndLink A B) C) (Implication (AndLink A B) C))), (: (ConjunctionIntroduction a a) (AndLink B B)), (: (ConjunctionIntroduction a cde) (AndLink B (Implication (OrLink C D) E))), (: (ConjunctionIntroduction a a) (AndLink B A)), (: (ConjunctionIntroduction a abc) (AndLink B (Implication (AndLink A B) C))), (: (ConjunctionIntroduction cde a) (AndLink (Implication (OrLink C D) E) B)), (: (ConjunctionIntroduction cde cde) (AndLink (Implication (OrLink C D) E) (Implication (OrLink C D) E))), (: (ConjunctionIntroduction cde a) (AndLink (Implication (OrLink C D) E) A)), (: (ConjunctionIntroduction cde abc) (AndLink (Implication (OrLink C D) E) (Implication (AndLink A B) C))), (: (ConjunctionIntroduction a a) (AndLink A B)), (: (ConjunctionIntroduction a cde) (AndLink A (Implication (OrLink C D) E))), (: (ConjunctionIntroduction a a) (AndLink A A)), (: (ConjunctionIntroduction a abc) (AndLink A (Implication (AndLink A B) C))), (: (ConjunctionIntroduction abc a) (AndLink (Implication (AndLink A B) C) B)), (: (ConjunctionIntroduction abc cde) (AndLink (Implication (AndLink A B) C) (Implication (OrLink C D) E))), (: (ConjunctionIntroduction abc a) (AndLink (Implication (AndLink A B) C) A)), (: (ConjunctionIntroduction abc abc) (AndLink (Implication (AndLink A B) C) (Implication (AndLink A B) C)))]")
; (= 2 "0.37user 0.00system 0:00.37elapsed 100%CPU (0avgtext+0avgdata 26636maxresident)k")
; (= 2 "0inputs+0outputs (0major+3504minor)pagefaults 0swaps")
; (load_answer_file /home/deb12user/metta-wam/tests/baseline_compat/hyperon-mettalog_sanity/synth_buffer/synthesize.metta.answers /home/deb12user/metta-wam/tests/baseline_compat/hyperon-mettalog_sanity/synth_buffer/synthesize.metta)
;;; Import modules
;;; Define Nat
(: Nat Type)
; Action: load=metta_atom_asserted('&self',[:,'Nat','Type'])
(: Z Nat)
; Action: load=metta_atom_asserted('&self',[:,'Z','Nat'])
(: S
(-> Nat Nat))
; Action: load=metta_atom_asserted('&self',[:,'S',[->,'Nat','Nat']])
;;; Enumerate all programs up to a given depth that are consistent with
;;; the query, using the given axiom non-deterministic functions and rules.
;;;
;;; The arguments are:
;;;
;;; $query: an Atom under the form (: TERM TYPE). The atom may contain
;;; free variables within TERM and TYPE to form various sort of
;;; queries, such as:
;;; 1. Backward chaining: (: $term (Inheritance $x Mammal))
;;; 2. Forward chaining: (: ($rule $premise AXIOM) $type)
;;; 3. Mixed chaining: (: ($rule $premise AXIOM) (Inheritance $x Mammal))
;;; 4. Type checking: (: TERM TYPE)
;;; 5. Type inference: (: TERM $type)
;;;
;;; $kb: a nullary function to axiom, to non-deterministically pick up
;;; an axiom. An axiom is an Atom of the form (: TERM TYPE).
;;;
;;; $rb: a nullary function to rule, to non-deterministically pick up a
;;; rule. A rule is a function mapping premises to conclusion,
;;; where premises and conclusion have the form (: TERM TYPE).
;;;
;;; $depth: a Nat representing the maximum depth of the generated
;;; programs.
;;;
;;; TODO: recurse over curried rules instead of duplicating code over
;;; tuples.
(: synthesize
(-> $a
(-> $kt)
(-> $rt) Nat $a))
; Action: load=metta_atom_asserted('&self',[:,synthesize,[->,_a,[->,_kt],[->,_rt],'Nat',_a]])
;;; Nullary rule (axiom)
(=
(synthesize $query $kb $rb $depth)
(let $query
($kb) $query))
; Action: load=metta_atom_asserted('&self',[=,[synthesize,_query,_kb,_rb,_depth],[let,_query,[_kb],_query]])
;;; Unary rule
(=
(synthesize $query $kb $rb
(S $k))
(let*
( ( (: $ructor
(-> $premise $conclusion)) ($rb))
( (:
($ructor $proof) $conclusion) $query)
( (: $proof $premise) (synthesize (: $proof $premise) $kb $rb $k))) $query))
; Action: load=metta_atom_asserted('&self',[=,[synthesize,_query,_kb,_rb,['S',_k]],['let*',[[[:,_ructor,[->,_premise,_conclusion]],[_rb]],[[:,[_ructor,_proof],_conclusion],_query],[[:,_proof,_premise],[synthesize,[:,_proof,_premise],_kb,_rb,_k]]],_query]])
;;; Binary rule
(=
(synthesize $query $kb $rb
(S $k))
(let*
( ( (: $ructor
(-> $premise1 $premise2 $conclusion)) ($rb))
( (:
($ructor $proof1 $proof2) $conclusion) $query)
( (: $proof1 $premise1) (synthesize (: $proof1 $premise1) $kb $rb $k))
( (: $proof2 $premise2) (synthesize (: $proof2 $premise2) $kb $rb $k))) $query))
; Action: load=metta_atom_asserted('&self',[=,[synthesize,_query,_kb,_rb,['S',_k]],['let*',[[[:,_ructor,[->,_premise1,_premise2,_conclusion]],[_rb]],[[:,[_ructor,_proof1,_proof2],_conclusion],_query],[[:,_proof1,_premise1],[synthesize,[:,_proof1,_premise1],_kb,_rb,_k]],[[:,_proof2,_premise2],[synthesize,[:,_proof2,_premise2],_kb,_rb,_k]]],_query]])
;;; Trinary rule
(=
(synthesize $query $kb $rb
(S $k))
(let*
( ( (: $ructor
(-> $premise1 $premise2 $premise3 $conclusion)) ($rb))
( (:
($ructor $proof1 $proof2 $proof3) $conclusion) $query)
( (: $proof1 $premise1) (synthesize (: $proof1 $premise1) $kb $rb $k))
( (: $proof2 $premise2) (synthesize (: $proof2 $premise2) $kb $rb $k))
( (: $proof3 $premise3) (synthesize (: $proof3 $premise3) $kb $rb $k))) $query))
; Action: load=metta_atom_asserted('&self',[=,[synthesize,_query,_kb,_rb,['S',_k]],['let*',[[[:,_ructor,[->,_premise1,_premise2,_premise3,_conclusion]],[_rb]],[[:,[_ructor,_proof1,_proof2,_proof3],_conclusion],_query],[[:,_proof1,_premise1],[synthesize,[:,_proof1,_premise1],_kb,_rb,_k]],[[:,_proof2,_premise2],[synthesize,[:,_proof2,_premise2],_kb,_rb,_k]],[[:,_proof3,_premise3],[synthesize,[:,_proof3,_premise3],_kb,_rb,_k]]],_query]])
;;; Quaternary rule
(=
(synthesize $query $kb $rb
(S $k))
(let*
( ( (: $ructor
(-> $premise1 $premise2 $premise3 $premise4 $conclusion)) ($rb))
( (:
($ructor $proof1 $proof2 $proof3 $proof4) $conclusion) $query)
( (: $proof1 $premise1) (synthesize (: $proof1 $premise1) $kb $rb $k))
( (: $proof2 $premise2) (synthesize (: $proof2 $premise2) $kb $rb $k))
( (: $proof3 $premise3) (synthesize (: $proof3 $premise3) $kb $rb $k))
( (: $proof4 $premise4) (synthesize (: $proof4 $premise4) $kb $rb $k))) $query))
; Action: load=metta_atom_asserted('&self',[=,[synthesize,_query,_kb,_rb,['S',_k]],['let*',[[[:,_ructor,[->,_premise1,_premise2,_premise3,_premise4,_conclusion]],[_rb]],[[:,[_ructor,_proof1,_proof2,_proof3,_proof4],_conclusion],_query],[[:,_proof1,_premise1],[synthesize,[:,_proof1,_premise1],_kb,_rb,_k]],[[:,_proof2,_premise2],[synthesize,[:,_proof2,_premise2],_kb,_rb,_k]],[[:,_proof3,_premise3],[synthesize,[:,_proof3,_premise3],_kb,_rb,_k]],[[:,_proof4,_premise4],[synthesize,[:,_proof4,_premise4],_kb,_rb,_k]]],_query]])
;;; Quintenary rule
(=
(synthesize $query $kb $rb
(S $k))
(let*
( ( (: $ructor
(-> $premise1 $premise2 $premise3 $premise4 $premise5 $conclusion)) ($rb))
( (:
($ructor $proof1 $proof2 $proof3 $proof4 $proof5) $conclusion) $query)
( (: $proof1 $premise1) (synthesize (: $proof1 $premise1) $kb $rb $k))
( (: $proof2 $premise2) (synthesize (: $proof2 $premise2) $kb $rb $k))
( (: $proof3 $premise3) (synthesize (: $proof3 $premise3) $kb $rb $k))
( (: $proof4 $premise4) (synthesize (: $proof4 $premise4) $kb $rb $k))
( (: $proof5 $premise5) (synthesize (: $proof5 $premise5) $kb $rb $k))) $query))
; Action: load=metta_atom_asserted('&self',[=,[synthesize,_query,_kb,_rb,['S',_k]],['let*',[[[:,_ructor,[->,_premise1,_premise2,_premise3,_premise4,_premise5,_conclusion]],[_rb]],[[:,[_ructor,_proof1,_proof2,_proof3,_proof4,_proof5],_conclusion],_query],[[:,_proof1,_premise1],[synthesize,[:,_proof1,_premise1],_kb,_rb,_k]],[[:,_proof2,_premise2],[synthesize,[:,_proof2,_premise2],_kb,_rb,_k]],[[:,_proof3,_premise3],[synthesize,[:,_proof3,_premise3],_kb,_rb,_k]],[[:,_proof4,_premise4],[synthesize,[:,_proof4,_premise4],_kb,_rb,_k]],[[:,_proof5,_premise5],[synthesize,[:,_proof5,_premise5],_kb,_rb,_k]]],_query]])
(: kb
(-> Atom))
; Action: load=metta_atom_asserted('&self',[:,kb,[->,'Atom']])
(=
(kb)
(: a A))
; Action: load=metta_atom_asserted('&self',[=,[kb],[:,a,'A']])
(=
(kb)
(: a B))
; Action: load=metta_atom_asserted('&self',[=,[kb],[:,a,'B']])
(=
(kb)
(: abc
(Implication
(AndLink A B) C)))
; Action: load=metta_atom_asserted('&self',[=,[kb],[:,abc,['Implication',['AndLink','A','B'],'C']]])
(=
(kb)
(: cde
(Implication
(OrLink C D) E)))
; Action: load=metta_atom_asserted('&self',[=,[kb],[:,cde,['Implication',['OrLink','C','D'],'E']]])
(: rb
(-> Atom))
; Action: load=metta_atom_asserted('&self',[:,rb,[->,'Atom']])
(=
(rb)
(: ModusPonens
(->
(ImplicationLink $p $q) $p $q)))
; Action: load=metta_atom_asserted('&self',[=,[rb],[:,'ModusPonens',[->,['ImplicationLink',_p,_q],_p,_q]]])
(=
(rb)
(: Deduction
(->
(ImplicationLink $p $q)
(ImplicationLink $q $r)
(ImplicationLink $p $r))))
; Action: load=metta_atom_asserted('&self',[=,[rb],[:,'Deduction',[->,['ImplicationLink',_p,_q],['ImplicationLink',_q,_r],['ImplicationLink',_p,_r]]]])
(=
(rb)
(: DisjunctiveSyllogism
(->
(OrLink $p $q)
(NotLink $p) $q)))
; Action: load=metta_atom_asserted('&self',[=,[rb],[:,'DisjunctiveSyllogism',[->,['OrLink',_p,_q],['NotLink',_p],_q]]])
(=
(rb)
(: DisjunctiveSyllogism
(->
(OrLink $p $q)
(NotLink $q) $p)))
; Action: load=metta_atom_asserted('&self',[=,[rb],[:,'DisjunctiveSyllogism',[->,['OrLink',_p,_q],['NotLink',_q],_p]]])
(=
(rb)
(: ConjunctionIntroduction
(-> $p $q
(AndLink $p $q))))
; Action: load=metta_atom_asserted('&self',[=,[rb],[:,'ConjunctionIntroduction',[->,_p,_q,['AndLink',_p,_q]]]])
(=
(rb)
(: ConjunctionEliminationLeft
(->
(AndLink $p $q) $p)))
; Action: load=metta_atom_asserted('&self',[=,[rb],[:,'ConjunctionEliminationLeft',[->,['AndLink',_p,_q],_p]]])
(=
(rb)
(: ConjunctionEliminationRight
(->
(AndLink $p $q) $q)))
; Action: load=metta_atom_asserted('&self',[=,[rb],[:,'ConjunctionEliminationRight',[->,['AndLink',_p,_q],_q]]])
(=
(rb)
(: DisjunctionIntroduction
(-> $p $q
(OrLink $p $q))))
; Action: load=metta_atom_asserted('&self',[=,[rb],[:,'DisjunctionIntroduction',[->,_p,_q,['OrLink',_p,_q]]]])
;; In file as:
!(synthesize
(: $term $type) kb rb
(S Z))
;; To unit test case:
!(assertEqualToResult
(synthesize
(: $term $type) kb rb
(S Z))
( (: a B)
(: cde
(Implication
(OrLink C D) E))
(: a A)
(: abc
(Implication
(AndLink A B) C))
(:
(DisjunctionIntroduction a a)
(OrLink B B))
(:
(DisjunctionIntroduction a cde)
(OrLink B
(Implication
(OrLink C D) E)))
(:
(DisjunctionIntroduction a a)
(OrLink B A))
(:
(DisjunctionIntroduction a abc)
(OrLink B
(Implication
(AndLink A B) C)))
(:
(DisjunctionIntroduction cde a)
(OrLink
(Implication
(OrLink C D) E) B))
(:
(DisjunctionIntroduction cde cde)
(OrLink
(Implication
(OrLink C D) E)
(Implication
(OrLink C D) E)))
(:
(DisjunctionIntroduction cde a)
(OrLink
(Implication
(OrLink C D) E) A))
(:
(DisjunctionIntroduction cde abc)
(OrLink
(Implication
(OrLink C D) E)
(Implication
(AndLink A B) C)))
(:
(DisjunctionIntroduction a a)
(OrLink A B))
(:
(DisjunctionIntroduction a cde)
(OrLink A
(Implication
(OrLink C D) E)))
(:
(DisjunctionIntroduction a a)
(OrLink A A))
(:
(DisjunctionIntroduction a abc)
(OrLink A
(Implication
(AndLink A B) C)))
(:
(DisjunctionIntroduction abc a)
(OrLink
(Implication
(AndLink A B) C) B))
(:
(DisjunctionIntroduction abc cde)
(OrLink
(Implication
(AndLink A B) C)
(Implication
(OrLink C D) E)))
(:
(DisjunctionIntroduction abc a)
(OrLink
(Implication
(AndLink A B) C) A))
(:
(DisjunctionIntroduction abc abc)
(OrLink
(Implication
(AndLink A B) C)
(Implication
(AndLink A B) C)))
(:
(ConjunctionIntroduction a a)
(AndLink B B))
(:
(ConjunctionIntroduction a cde)
(AndLink B
(Implication
(OrLink C D) E)))
(:
(ConjunctionIntroduction a a)
(AndLink B A))
(:
(ConjunctionIntroduction a abc)
(AndLink B
(Implication
(AndLink A B) C)))
(:
(ConjunctionIntroduction cde a)
(AndLink
(Implication
(OrLink C D) E) B))
(:
(ConjunctionIntroduction cde cde)
(AndLink
(Implication
(OrLink C D) E)
(Implication
(OrLink C D) E)))
(:
(ConjunctionIntroduction cde a)
(AndLink
(Implication
(OrLink C D) E) A))
(:
(ConjunctionIntroduction cde abc)
(AndLink
(Implication
(OrLink C D) E)
(Implication
(AndLink A B) C)))
(:
(ConjunctionIntroduction a a)
(AndLink A B))
(:
(ConjunctionIntroduction a cde)
(AndLink A
(Implication
(OrLink C D) E)))
(:
(ConjunctionIntroduction a a)
(AndLink A A))
(:
(ConjunctionIntroduction a abc)
(AndLink A
(Implication
(AndLink A B) C)))
(:
(ConjunctionIntroduction abc a)
(AndLink
(Implication
(AndLink A B) C) B))
(:
(ConjunctionIntroduction abc cde)
(AndLink
(Implication
(AndLink A B) C)
(Implication
(OrLink C D) E)))
(:
(ConjunctionIntroduction abc a)
(AndLink
(Implication
(AndLink A B) C) A))
(:
(ConjunctionIntroduction abc abc)
(AndLink
(Implication
(AndLink A B) C)
(Implication
(AndLink A B) C)))))
[
;;; SYNTH-BUFFER.SYNTHESIZE.01
;
; EVAL TEST
; took 0.117 secs. (117.48 milliseconds)
!(assertEqualToResult
(synthesize
(: $term $type) kb rb
(S Z))
( (: a B)
(: cde
(Implication
(OrLink C D) E))
(: a A)
(: abc
(Implication
(AndLink A B) C))
(:
(DisjunctionIntroduction a a)
(OrLink B B))
(:
(DisjunctionIntroduction a cde)
(OrLink B
(Implication
(OrLink C D) E)))
(:
(DisjunctionIntroduction a a)
(OrLink B A))
(:
(DisjunctionIntroduction a abc)
(OrLink B
(Implication
(AndLink A B) C)))
(:
(DisjunctionIntroduction cde a)
(OrLink
(Implication
(OrLink C D) E) B))
(:
(DisjunctionIntroduction cde cde)
(OrLink
(Implication
(OrLink C D) E)
(Implication
(OrLink C D) E)))
(:
(DisjunctionIntroduction cde a)
(OrLink
(Implication
(OrLink C D) E) A))
(:
(DisjunctionIntroduction cde abc)
(OrLink
(Implication
(OrLink C D) E)
(Implication
(AndLink A B) C)))
(:
(DisjunctionIntroduction a a)
(OrLink A B))
(:
(DisjunctionIntroduction a cde)
(OrLink A
(Implication
(OrLink C D) E)))
(:
(DisjunctionIntroduction a a)
(OrLink A A))
(:
(DisjunctionIntroduction a abc)
(OrLink A
(Implication
(AndLink A B) C)))
(:
(DisjunctionIntroduction abc a)
(OrLink
(Implication
(AndLink A B) C) B))
(:
(DisjunctionIntroduction abc cde)
(OrLink
(Implication
(AndLink A B) C)
(Implication
(OrLink C D) E)))
(:
(DisjunctionIntroduction abc a)
(OrLink
(Implication
(AndLink A B) C) A))
(:
(DisjunctionIntroduction abc abc)
(OrLink
(Implication
(AndLink A B) C)
(Implication
(AndLink A B) C)))
(:
(ConjunctionIntroduction a a)
(AndLink B B))
(:
(ConjunctionIntroduction a cde)
(AndLink B
(Implication
(OrLink C D) E)))
(:
(ConjunctionIntroduction a a)
(AndLink B A))
(:
(ConjunctionIntroduction a abc)
(AndLink B
(Implication
(AndLink A B) C)))
(:
(ConjunctionIntroduction cde a)
(AndLink
(Implication
(OrLink C D) E) B))
(:
(ConjunctionIntroduction cde cde)
(AndLink
(Implication
(OrLink C D) E)
(Implication
(OrLink C D) E)))
(:
(ConjunctionIntroduction cde a)
(AndLink
(Implication
(OrLink C D) E) A))
(:
(ConjunctionIntroduction cde abc)
(AndLink
(Implication
(OrLink C D) E)
(Implication
(AndLink A B) C)))
(:
(ConjunctionIntroduction a a)
(AndLink A B))
(:
(ConjunctionIntroduction a cde)
(AndLink A
(Implication
(OrLink C D) E)))
(:
(ConjunctionIntroduction a a)
(AndLink A A))
(:
(ConjunctionIntroduction a abc)
(AndLink A
(Implication
(AndLink A B) C)))
(:
(ConjunctionIntroduction abc a)
(AndLink
(Implication
(AndLink A B) C) B))
(:
(ConjunctionIntroduction abc cde)
(AndLink
(Implication
(AndLink A B) C)
(Implication
(OrLink C D) E)))
(:
(ConjunctionIntroduction abc a)
(AndLink
(Implication
(AndLink A B) C) A))
(:
(ConjunctionIntroduction abc abc)
(AndLink
(Implication
(AndLink A B) C)
(Implication
(AndLink A B) C)))))
(loonit_success
(equal_enough_for_test
( (: a A)
(: a B)
(: abc
(Implication
(AndLink A B) C))
(: cde
(Implication
(OrLink C D) E))
(:
(ConjunctionIntroduction a a)
(AndLink A A))
(:
(ConjunctionIntroduction a a)
(AndLink A B))
(:
(ConjunctionIntroduction a abc)
(AndLink A
(Implication
(AndLink A B) C)))
(:
(ConjunctionIntroduction a cde)
(AndLink A
(Implication
(OrLink C D) E)))
(:
(ConjunctionIntroduction a a)
(AndLink B A))
(:
(ConjunctionIntroduction a a)
(AndLink B B))
(:
(ConjunctionIntroduction a abc)
(AndLink B
(Implication
(AndLink A B) C)))
(:
(ConjunctionIntroduction a cde)
(AndLink B
(Implication
(OrLink C D) E)))
(:
(ConjunctionIntroduction abc a)
(AndLink
(Implication
(AndLink A B) C) A))
(:
(ConjunctionIntroduction abc a)
(AndLink
(Implication
(AndLink A B) C) B))
(:
(ConjunctionIntroduction abc abc)
(AndLink
(Implication
(AndLink A B) C)
(Implication
(AndLink A B) C)))
(:
(ConjunctionIntroduction abc cde)
(AndLink
(Implication
(AndLink A B) C)
(Implication
(OrLink C D) E)))
(:
(ConjunctionIntroduction cde a)
(AndLink
(Implication
(OrLink C D) E) A))
(:
(ConjunctionIntroduction cde a)
(AndLink
(Implication
(OrLink C D) E) B))
(:
(ConjunctionIntroduction cde abc)
(AndLink
(Implication
(OrLink C D) E)
(Implication
(AndLink A B) C)))
(:
(ConjunctionIntroduction cde cde)
(AndLink
(Implication
(OrLink C D) E)
(Implication
(OrLink C D) E)))
(:
(DisjunctionIntroduction a a)
(OrLink A A))
(:
(DisjunctionIntroduction a a)
(OrLink A B))
(:
(DisjunctionIntroduction a abc)
(OrLink A
(Implication
(AndLink A B) C)))
(:
(DisjunctionIntroduction a cde)
(OrLink A
(Implication
(OrLink C D) E)))
(:
(DisjunctionIntroduction a a)
(OrLink B A))
(:
(DisjunctionIntroduction a a)
(OrLink B B))
(:
(DisjunctionIntroduction a abc)
(OrLink B
(Implication
(AndLink A B) C)))
(:
(DisjunctionIntroduction a cde)
(OrLink B
(Implication
(OrLink C D) E)))
(:
(DisjunctionIntroduction abc a)
(OrLink
(Implication
(AndLink A B) C) A))
(:
(DisjunctionIntroduction abc a)
(OrLink
(Implication
(AndLink A B) C) B))
(:
(DisjunctionIntroduction abc abc)
(OrLink
(Implication
(AndLink A B) C)
(Implication
(AndLink A B) C)))
(:
(DisjunctionIntroduction abc cde)
(OrLink
(Implication
(AndLink A B) C)
(Implication
(OrLink C D) E)))
(:
(DisjunctionIntroduction cde a)
(OrLink
(Implication
(OrLink C D) E) A))
(:
(DisjunctionIntroduction cde a)
(OrLink
(Implication
(OrLink C D) E) B))
(:
(DisjunctionIntroduction cde abc)
(OrLink
(Implication
(OrLink C D) E)
(Implication
(AndLink A B) C)))
(:
(DisjunctionIntroduction cde cde)
(OrLink
(Implication
(OrLink C D) E)
(Implication
(OrLink C D) E))))
( (: a B)
(: cde
(Implication
(OrLink C D) E))
(: a A)
(: abc
(Implication
(AndLink A B) C))
(:
(DisjunctionIntroduction a a)
(OrLink B B))
(:
(DisjunctionIntroduction a cde)
(OrLink B
(Implication
(OrLink C D) E)))
(:
(DisjunctionIntroduction a a)
(OrLink B A))
(:
(DisjunctionIntroduction a abc)
(OrLink B
(Implication
(AndLink A B) C)))
(:
(DisjunctionIntroduction cde a)
(OrLink
(Implication
(OrLink C D) E) B))
(:
(DisjunctionIntroduction cde cde)
(OrLink
(Implication
(OrLink C D) E)
(Implication
(OrLink C D) E)))
(:
(DisjunctionIntroduction cde a)
(OrLink
(Implication
(OrLink C D) E) A))
(:
(DisjunctionIntroduction cde abc)
(OrLink
(Implication
(OrLink C D) E)
(Implication
(AndLink A B) C)))
(:
(DisjunctionIntroduction a a)
(OrLink A B))
(:
(DisjunctionIntroduction a cde)
(OrLink A
(Implication
(OrLink C D) E)))
(:
(DisjunctionIntroduction a a)
(OrLink A A))
(:
(DisjunctionIntroduction a abc)
(OrLink A
(Implication
(AndLink A B) C)))
(:
(DisjunctionIntroduction abc a)
(OrLink
(Implication
(AndLink A B) C) B))
(:
(DisjunctionIntroduction abc cde)
(OrLink
(Implication
(AndLink A B) C)
(Implication
(OrLink C D) E)))
(:
(DisjunctionIntroduction abc a)
(OrLink
(Implication
(AndLink A B) C) A))
(:
(DisjunctionIntroduction abc abc)
(OrLink
(Implication
(AndLink A B) C)
(Implication
(AndLink A B) C)))
(:
(ConjunctionIntroduction a a)
(AndLink B B))
(:
(ConjunctionIntroduction a cde)
(AndLink B
(Implication
(OrLink C D) E)))
(:
(ConjunctionIntroduction a a)
(AndLink B A))
(:
(ConjunctionIntroduction a abc)
(AndLink B
(Implication
(AndLink A B) C)))
(:
(ConjunctionIntroduction cde a)
(AndLink
(Implication
(OrLink C D) E) B))
(:
(ConjunctionIntroduction cde cde)
(AndLink
(Implication
(OrLink C D) E)
(Implication
(OrLink C D) E)))
(:
(ConjunctionIntroduction cde a)
(AndLink
(Implication
(OrLink C D) E) A))
(:
(ConjunctionIntroduction cde abc)
(AndLink
(Implication
(OrLink C D) E)
(Implication
(AndLink A B) C)))
(:
(ConjunctionIntroduction a a)
(AndLink A B))
(:
(ConjunctionIntroduction a cde)
(AndLink A
(Implication
(OrLink C D) E)))
(:
(ConjunctionIntroduction a a)
(AndLink A A))
(:
(ConjunctionIntroduction a abc)
(AndLink A
(Implication
(AndLink A B) C)))
(:
(ConjunctionIntroduction abc a)
(AndLink
(Implication
(AndLink A B) C) B))
(:
(ConjunctionIntroduction abc cde)
(AndLink
(Implication
(AndLink A B) C)
(Implication
(OrLink C D) E)))
(:
(ConjunctionIntroduction abc a)
(AndLink
(Implication
(AndLink A B) C) A))
(:
(ConjunctionIntroduction abc abc)
(AndLink
(Implication
(AndLink A B) C)
(Implication
(AndLink A B) C))))))
Deterministic: ()()
; Execution took 0.179 secs. (178.93 milliseconds)
]
% 2,892,548 inferences, 0.531 CPU in 0.533 seconds (100% CPU, 5442470 Lips)
; (= /home/deb12user/metta-wam/tests/baseline_compat/hyperon-mettalog_sanity/synth_buffer/synthesize.metta 0)
LoonIt Report
------------
Successes: 1
Failures: 0
Return to summaries
; (is_cmd_option execute time --time=debug debug)
; (set_option_value time debug)
; (set_debug time true)
metta+>^D
; (is_cmd_option execute stdin --stdin=tty tty)
; (set_option_value stdin tty)
; (is_cmd_option execute stdout --stdout=tty tty)
; (set_option_value stdout tty)
; (is_cmd_option execute stderr --stderr=tty tty)
; (set_option_value stderr tty)
; (set_option_value prolog false)
; (set_option_value compat auto)
; (set_option_value compatio true)
; (maybe_halt 7)
Script done on 2024-09-03 05:34:37-07:00 [COMMAND_EXIT_CODE="7"]