Anne is big. Anne is furry. Anne is green. Anne is kind. Anne is nice. Anne is round. Anne is young. Harry is big. Harry is furry. Harry is green. Harry is kind. Harry is nice. Harry is round. Harry is young. All round people are furry. All young, big people are nice. If Anne is furry then Anne is round. Nice people are kind. If Harry is green and Harry is round then Harry is big. All round people are nice. All kind people are young. If Anne is big and Anne is nice then Anne is furry.
Anne is big.
("Anne" "is" "big" "+")
Anne is furry.
("Anne" "is" "furry" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is round.
("Anne" "is" "round" "+")
Anne is young.
("Anne" "is" "young" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is young.
("Harry" "is" "young" "+")
All round people are furry.
((("someone" "is" "round" "+")) -> ("someone" "is" "furry" "+"))
All young, big people are nice.
((("someone" "is" "young" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "nice" "+"))
If Anne is furry then Anne is round.
((("Anne" "is" "furry" "+")) -> ("Anne" "is" "round" "+"))
Nice people are kind.
((("someone" "is" "nice" "+")) -> ("someone" "is" "kind" "+"))
If Harry is green and Harry is round then Harry is big.
((("Harry" "is" "green" "+") ("Harry" "is" "round" "+")) -> ("Harry" "is" "big" "+"))
All round people are nice.
((("someone" "is" "round" "+")) -> ("someone" "is" "nice" "+"))
All kind people are young.
((("someone" "is" "kind" "+")) -> ("someone" "is" "young" "+"))
If Anne is big and Anne is nice then Anne is furry.
((("Anne" "is" "big" "+") ("Anne" "is" "nice" "+")) -> ("Anne" "is" "furry" "+"))
Harry is big.
True
1
proof
[(triple8 OR ((triple10 triple13) -> rule5))]
("Harry" "is" "big" "+")
triple8
((triple10 triple13) -> (rule5 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is not nice.
False
1
inv-proof
[(triple12 OR ((triple13) -> rule6) OR ((triple14 triple8) -> rule2) OR ((triple14 ((triple10 triple13) -> rule5)) -> rule2) OR ((((triple11) -> rule7) triple8) -> rule2) OR ((((triple11) -> rule7) ((triple10 triple13) -> rule5)) -> rule2))]
("Harry" "is" "nice" "-")
triple12
((triple13) -> (rule6 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
((triple14 triple8) -> (rule2 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
((triple14 ((triple10 triple13) -> (rule5 % int2))) -> (rule2 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
((((triple11) -> (rule7 % int2)) triple8) -> (rule2 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
((((triple11) -> (rule7 % int3)) ((triple10 triple13) -> (rule5 % int2))) -> (rule2 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
@0: Anne is big.[(triple1)] Anne is furry.[(triple2 OR ((triple6) -> rule1) OR ((triple1 triple5) -> rule8) OR ((triple1 ((triple6) -> rule6)) -> rule8) OR ((triple1 ((triple7 triple1) -> rule2)) -> rule8) OR ((triple1 ((((triple4) -> rule7) triple1) -> rule2)) -> rule8))] Anne is green.[(triple3)] Anne is kind.[(triple4 OR ((triple5) -> rule4) OR ((((triple6) -> rule6)) -> rule4) OR ((((triple7 triple1) -> rule2)) -> rule4) OR ((((((triple2) -> rule3)) -> rule6)) -> rule4))] Anne is nice.[(triple5 OR ((triple6) -> rule6) OR ((triple7 triple1) -> rule2) OR ((((triple2) -> rule3)) -> rule6) OR ((((triple4) -> rule7) triple1) -> rule2))] Anne is round.[(triple6 OR ((triple2) -> rule3) OR ((((triple1 triple5) -> rule8)) -> rule3) OR ((((triple1 ((triple7 triple1) -> rule2)) -> rule8)) -> rule3) OR ((((triple1 ((((triple4) -> rule7) triple1) -> rule2)) -> rule8)) -> rule3))] Anne is young.[(triple7 OR ((triple4) -> rule7) OR ((((triple5) -> rule4)) -> rule7) OR ((((((triple6) -> rule6)) -> rule4)) -> rule7) OR ((((((((triple2) -> rule3)) -> rule6)) -> rule4)) -> rule7))] Harry is big.[(triple8 OR ((triple10 triple13) -> rule5))] Harry is furry.[(triple9 OR ((triple13) -> rule1))] Harry is green.[(triple10)] Harry is kind.[(triple11 OR ((triple12) -> rule4) OR ((((triple13) -> rule6)) -> rule4) OR ((((triple14 triple8) -> rule2)) -> rule4) OR ((((triple14 ((triple10 triple13) -> rule5)) -> rule2)) -> rule4))] Harry is nice.[(triple12 OR ((triple13) -> rule6) OR ((triple14 triple8) -> rule2) OR ((triple14 ((triple10 triple13) -> rule5)) -> rule2) OR ((((triple11) -> rule7) triple8) -> rule2) OR ((((triple11) -> rule7) ((triple10 triple13) -> rule5)) -> rule2))] Harry is round.[(triple13)] Harry is young.[(triple14 OR ((triple11) -> rule7) OR ((((triple12) -> rule4)) -> rule7) OR ((((((triple13) -> rule6)) -> rule4)) -> rule7))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is furry.
("Anne" "is" "furry" "+")
triple2
((triple6) -> (rule1 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
((triple1 triple5) -> (rule8 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
((triple1 ((triple6) -> (rule6 % int2))) -> (rule8 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
((triple1 ((triple7 triple1) -> (rule2 % int2))) -> (rule8 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
((triple1 ((((triple4) -> (rule7 % int3)) triple1) -> (rule2 % int2))) -> (rule8 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Anne is green.
("Anne" "is" "green" "+")
triple3
Anne is kind.
("Anne" "is" "kind" "+")
triple4
((triple5) -> (rule4 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
((((triple6) -> (rule6 % int2))) -> (rule4 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
((((triple7 triple1) -> (rule2 % int2))) -> (rule4 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
((((((triple2) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
int3
Anne is nice.
("Anne" "is" "nice" "+")
triple5
((triple6) -> (rule6 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
((triple7 triple1) -> (rule2 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
((((triple2) -> (rule3 % int2))) -> (rule6 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
((((triple4) -> (rule7 % int2)) triple1) -> (rule2 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
triple6
((triple2) -> (rule3 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
((((triple1 triple5) -> (rule8 % int2))) -> (rule3 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
((((triple1 ((triple7 triple1) -> (rule2 % int3))) -> (rule8 % int2))) -> (rule3 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
((((triple1 ((((triple4) -> (rule7 % int4)) triple1) -> (rule2 % int3))) -> (rule8 % int2))) -> (rule3 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
Anne is young.
("Anne" "is" "young" "+")
int4
Anne is young.
("Anne" "is" "young" "+")
triple7
((triple4) -> (rule7 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
((((triple5) -> (rule4 % int2))) -> (rule7 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
((((((triple6) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
((((((((triple2) -> (rule3 % int4))) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
Anne is round.
("Anne" "is" "round" "+")
int4
Harry is big.
("Harry" "is" "big" "+")
triple8
((triple10 triple13) -> (rule5 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
triple9
((triple13) -> (rule1 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
triple10
Harry is kind.
("Harry" "is" "kind" "+")
triple11
((triple12) -> (rule4 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
((((triple13) -> (rule6 % int2))) -> (rule4 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
((((triple14 triple8) -> (rule2 % int2))) -> (rule4 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
((((triple14 ((triple10 triple13) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
Harry is nice.
("Harry" "is" "nice" "+")
triple12
((triple13) -> (rule6 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
((triple14 triple8) -> (rule2 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
((triple14 ((triple10 triple13) -> (rule5 % int2))) -> (rule2 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
((((triple11) -> (rule7 % int2)) triple8) -> (rule2 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
((((triple11) -> (rule7 % int3)) ((triple10 triple13) -> (rule5 % int2))) -> (rule2 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
Harry is round.
("Harry" "is" "round" "+")
triple13
Harry is young.
("Harry" "is" "young" "+")
triple14
((triple11) -> (rule7 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
((((triple12) -> (rule4 % int2))) -> (rule7 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
((((((triple13) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3