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