Bob is big. Bob is cold. Bob is furry. Bob is green. Bob is rough. Bob is round. Harry is cold. Harry is furry. Harry is green. Harry is red. Harry is rough. Harry is round. All big, round things are red. If something is furry and big then it is red. If something is rough and green then it is furry. Rough things are big. All furry things are green. If Bob is red then Bob is rough. All big, furry things are cold. If something is big and rough then it is round.
Bob is big.
("Bob" "is" "big" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is round.
("Bob" "is" "round" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is round.
("Harry" "is" "round" "+")
All big, round things are red.
((("something" "is" "big" "+") ("something" "is" "round" "+")) -> ("something" "is" "red" "+"))
If something is furry and big then it is red.
((("something" "is" "furry" "+") ("something" "is" "big" "+")) -> ("something" "is" "red" "+"))
If something is rough and green then it is furry.
((("something" "is" "rough" "+") ("something" "is" "green" "+")) -> ("something" "is" "furry" "+"))
Rough things are big.
((("something" "is" "rough" "+")) -> ("something" "is" "big" "+"))
All furry things are green.
((("something" "is" "furry" "+")) -> ("something" "is" "green" "+"))
If Bob is red then Bob is rough.
((("Bob" "is" "red" "+")) -> ("Bob" "is" "rough" "+"))
All big, furry things are cold.
((("something" "is" "big" "+") ("something" "is" "furry" "+")) -> ("something" "is" "cold" "+"))
If something is big and rough then it is round.
((("something" "is" "big" "+") ("something" "is" "rough" "+")) -> ("something" "is" "round" "+"))
Harry is round.
True
1
proof
[(triple12 OR ((((triple11) -> rule4) triple11) -> rule8))]
("Harry" "is" "round" "+")
triple12
((((triple11) -> (rule4 % int2)) triple11) -> (rule8 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is not red.
False
1
inv-proof
[(triple10 OR ((triple8 ((triple11) -> rule4)) -> rule2) OR ((((triple11) -> rule4) triple12) -> rule1) OR ((((triple11 triple9) -> rule3) ((triple11) -> rule4)) -> rule2) OR ((((triple11) -> rule4) ((((triple11) -> rule4) triple11) -> rule8)) -> rule1))]
("Harry" "is" "red" "-")
triple10
((triple8 ((triple11) -> (rule4 % int2))) -> (rule2 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
((((triple11) -> (rule4 % int2)) triple12) -> (rule1 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
((((triple11 triple9) -> (rule3 % int3)) ((triple11) -> (rule4 % int2))) -> (rule2 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
((((triple11) -> (rule4 % int3)) ((((triple11) -> (rule4 % int3)) triple11) -> (rule8 % int2))) -> (rule1 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
Bob is red.
True
3
proof
[(((triple1 triple6) -> rule1) OR ((triple3 triple1) -> rule2) OR ((triple1 ((triple1 triple5) -> rule8)) -> rule1) OR ((triple3 ((triple5) -> rule4)) -> rule2) OR ((((triple5) -> rule4) triple6) -> rule1) OR ((((triple5 triple4) -> rule3) triple1) -> rule2) OR ((((triple5) -> rule4) ((triple1 triple5) -> rule8)) -> rule1) OR ((((triple5 triple4) -> rule3) ((triple5) -> rule4)) -> rule2) OR ((triple1 ((((triple5) -> rule4) triple5) -> rule8)) -> rule1) OR ((((triple5) -> rule4) ((((triple5) -> rule4) triple5) -> rule8)) -> rule1))]
("Bob" "is" "red" "+")
((triple1 triple6) -> (rule1 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
((triple3 triple1) -> (rule2 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
((triple1 ((triple1 triple5) -> (rule8 % int2))) -> (rule1 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
((triple3 ((triple5) -> (rule4 % int2))) -> (rule2 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
((((triple5) -> (rule4 % int2)) triple6) -> (rule1 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
((((triple5 triple4) -> (rule3 % int2)) triple1) -> (rule2 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
((((triple5) -> (rule4 % int3)) ((triple1 triple5) -> (rule8 % int2))) -> (rule1 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
((((triple5 triple4) -> (rule3 % int3)) ((triple5) -> (rule4 % int2))) -> (rule2 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
((triple1 ((((triple5) -> (rule4 % int3)) triple5) -> (rule8 % int2))) -> (rule1 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
((((triple5) -> (rule4 % int3)) ((((triple5) -> (rule4 % int3)) triple5) -> (rule8 % int2))) -> (rule1 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
Harry is not big.
False
2
inv-proof
[(((triple11) -> rule4))]
("Harry" "is" "big" "-")
((triple11) -> (rule4 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
@0: Bob is big.[(triple1 OR ((triple5) -> rule4))] Bob is cold.[(triple2 OR ((triple1 triple3) -> rule7) OR ((triple1 ((triple5 triple4) -> rule3)) -> rule7) OR ((((triple5) -> rule4) triple3) -> rule7) OR ((((triple5) -> rule4) ((triple5 triple4) -> rule3)) -> rule7) OR ((triple1 ((((((triple1 triple6) -> rule1)) -> rule6) triple4) -> rule3)) -> rule7) OR ((((triple5) -> rule4) ((((((triple1 triple6) -> rule1)) -> rule6) triple4) -> rule3)) -> rule7))] Bob is furry.[(triple3 OR ((triple5 triple4) -> rule3) OR ((((((triple1 triple6) -> rule1)) -> rule6) triple4) -> rule3))] Bob is green.[(triple4 OR ((triple3) -> rule5))] Bob is rough.[(triple5 OR ((((triple1 triple6) -> rule1)) -> rule6) OR ((((triple3 triple1) -> rule2)) -> rule6))] Bob is round.[(triple6 OR ((triple1 triple5) -> rule8) OR ((((triple5) -> rule4) triple5) -> rule8) OR ((triple1 ((((triple3 triple1) -> rule2)) -> rule6)) -> rule8) OR ((((triple5) -> rule4) ((((triple3 triple1) -> rule2)) -> rule6)) -> rule8))] Harry is cold.[(triple7 OR ((((triple11) -> rule4) triple8) -> rule7) OR ((((triple11) -> rule4) ((triple11 triple9) -> rule3)) -> rule7))] Harry is furry.[(triple8 OR ((triple11 triple9) -> rule3))] Harry is green.[(triple9 OR ((triple8) -> rule5))] Harry is red.[(triple10 OR ((triple8 ((triple11) -> rule4)) -> rule2) OR ((((triple11) -> rule4) triple12) -> rule1) OR ((((triple11 triple9) -> rule3) ((triple11) -> rule4)) -> rule2) OR ((((triple11) -> rule4) ((((triple11) -> rule4) triple11) -> rule8)) -> rule1))] Harry is rough.[(triple11)] Harry is round.[(triple12 OR ((((triple11) -> rule4) triple11) -> rule8))] @1: Bob is red.[(((triple1 triple6) -> rule1) OR ((triple3 triple1) -> rule2) OR ((triple1 ((triple1 triple5) -> rule8)) -> rule1) OR ((triple3 ((triple5) -> rule4)) -> rule2) OR ((((triple5) -> rule4) triple6) -> rule1) OR ((((triple5 triple4) -> rule3) triple1) -> rule2) OR ((((triple5) -> rule4) ((triple1 triple5) -> rule8)) -> rule1) OR ((((triple5 triple4) -> rule3) ((triple5) -> rule4)) -> rule2) OR ((triple1 ((((triple5) -> rule4) triple5) -> rule8)) -> rule1) OR ((((triple5) -> rule4) ((((triple5) -> rule4) triple5) -> rule8)) -> rule1))] Harry is big.[(((triple11) -> rule4))]
Bob is big.
("Bob" "is" "big" "+")
triple1
((triple5) -> (rule4 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
triple2
((triple1 triple3) -> (rule7 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
((triple1 ((triple5 triple4) -> (rule3 % int2))) -> (rule7 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
((((triple5) -> (rule4 % int2)) triple3) -> (rule7 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
((((triple5) -> (rule4 % int3)) ((triple5 triple4) -> (rule3 % int2))) -> (rule7 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
((triple1 ((((((triple1 triple6) -> (rule1 % int4))) -> (rule6 % int3)) triple4) -> (rule3 % int2))) -> (rule7 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
Bob is red.
("Bob" "is" "red" "+")
int4
((((triple5) -> (rule4 % int5)) ((((((triple1 triple6) -> (rule1 % int4))) -> (rule6 % int3)) triple4) -> (rule3 % int2))) -> (rule7 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
Bob is red.
("Bob" "is" "red" "+")
int4
Bob is big.
("Bob" "is" "big" "+")
int5
Bob is furry.
("Bob" "is" "furry" "+")
triple3
((triple5 triple4) -> (rule3 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
((((((triple1 triple6) -> (rule1 % int3))) -> (rule6 % int2)) triple4) -> (rule3 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
Bob is green.
("Bob" "is" "green" "+")
triple4
((triple3) -> (rule5 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
triple5
((((triple1 triple6) -> (rule1 % int2))) -> (rule6 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
((((triple3 triple1) -> (rule2 % int2))) -> (rule6 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
triple6
((triple1 triple5) -> (rule8 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
((((triple5) -> (rule4 % int2)) triple5) -> (rule8 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
((triple1 ((((triple3 triple1) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule8 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
((((triple5) -> (rule4 % int4)) ((((triple3 triple1) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule8 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
Bob is big.
("Bob" "is" "big" "+")
int4
Harry is cold.
("Harry" "is" "cold" "+")
triple7
((((triple11) -> (rule4 % int2)) triple8) -> (rule7 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
((((triple11) -> (rule4 % int3)) ((triple11 triple9) -> (rule3 % int2))) -> (rule7 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
Harry is furry.
("Harry" "is" "furry" "+")
triple8
((triple11 triple9) -> (rule3 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
triple9
((triple8) -> (rule5 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
triple10
((triple8 ((triple11) -> (rule4 % int2))) -> (rule2 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
((((triple11) -> (rule4 % int2)) triple12) -> (rule1 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
((((triple11 triple9) -> (rule3 % int3)) ((triple11) -> (rule4 % int2))) -> (rule2 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
((((triple11) -> (rule4 % int3)) ((((triple11) -> (rule4 % int3)) triple11) -> (rule8 % int2))) -> (rule1 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
Harry is rough.
("Harry" "is" "rough" "+")
triple11
Harry is round.
("Harry" "is" "round" "+")
triple12
((((triple11) -> (rule4 % int2)) triple11) -> (rule8 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
((triple1 triple6) -> (rule1 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
((triple3 triple1) -> (rule2 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
((triple1 ((triple1 triple5) -> (rule8 % int2))) -> (rule1 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
((triple3 ((triple5) -> (rule4 % int2))) -> (rule2 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
((((triple5) -> (rule4 % int2)) triple6) -> (rule1 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
((((triple5 triple4) -> (rule3 % int2)) triple1) -> (rule2 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
((((triple5) -> (rule4 % int3)) ((triple1 triple5) -> (rule8 % int2))) -> (rule1 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
((((triple5 triple4) -> (rule3 % int3)) ((triple5) -> (rule4 % int2))) -> (rule2 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
((triple1 ((((triple5) -> (rule4 % int3)) triple5) -> (rule8 % int2))) -> (rule1 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
((((triple5) -> (rule4 % int3)) ((((triple5) -> (rule4 % int3)) triple5) -> (rule8 % int2))) -> (rule1 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
Harry is big.
("Harry" "is" "big" "+")
((triple11) -> (rule4 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1