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