Bob is big. Bob is blue. Bob is cold. Bob is furry. Bob is red. Bob is white. Bob is young. All white, red things are cold. If Bob is furry and Bob is big then Bob is white. White, blue things are cold. Cold things are blue. If Bob is blue then Bob is red. Furry, cold things are big. If Bob is big and Bob is young then Bob is white. All big, cold things are blue.
Bob is big.
("Bob" "is" "big" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is white.
("Bob" "is" "white" "+")
Bob is young.
("Bob" "is" "young" "+")
All white, red things are cold.
((("something" "is" "white" "+") ("something" "is" "red" "+")) -> ("something" "is" "cold" "+"))
If Bob is furry and Bob is big then Bob is white.
((("Bob" "is" "furry" "+") ("Bob" "is" "big" "+")) -> ("Bob" "is" "white" "+"))
White, blue things are cold.
((("something" "is" "white" "+") ("something" "is" "blue" "+")) -> ("something" "is" "cold" "+"))
Cold things are blue.
((("something" "is" "cold" "+")) -> ("something" "is" "blue" "+"))
If Bob is blue then Bob is red.
((("Bob" "is" "blue" "+")) -> ("Bob" "is" "red" "+"))
Furry, cold things are big.
((("something" "is" "furry" "+") ("something" "is" "cold" "+")) -> ("something" "is" "big" "+"))
If Bob is big and Bob is young then Bob is white.
((("Bob" "is" "big" "+") ("Bob" "is" "young" "+")) -> ("Bob" "is" "white" "+"))
All big, cold things are blue.
((("something" "is" "big" "+") ("something" "is" "cold" "+")) -> ("something" "is" "blue" "+"))
Bob is white.
True
1
proof
[(triple6 OR ((triple1 triple7) -> rule7) OR ((triple4 triple1) -> rule2) OR ((triple4 ((triple4 triple3) -> rule6)) -> rule2) OR ((((triple4 triple3) -> rule6) triple7) -> rule7))]
("Bob" "is" "white" "+")
triple6
((triple1 triple7) -> (rule7 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
((triple4 triple1) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
((triple4 ((triple4 triple3) -> (rule6 % int2))) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
((((triple4 triple3) -> (rule6 % int2)) triple7) -> (rule7 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is not red.
False
1
inv-proof
[(triple5 OR ((triple2) -> rule5) OR ((((triple3) -> rule4)) -> rule5) OR ((((triple1 triple3) -> rule8)) -> rule5) OR ((((((triple4 triple3) -> rule6) triple3) -> rule8)) -> rule5))]
("Bob" "is" "red" "-")
triple5
((triple2) -> (rule5 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
((((triple3) -> (rule4 % int2))) -> (rule5 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
((((triple1 triple3) -> (rule8 % int2))) -> (rule5 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
((((((triple4 triple3) -> (rule6 % int3)) triple3) -> (rule8 % int2))) -> (rule5 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
@0: Bob is big.[(triple1 OR ((triple4 triple3) -> rule6) OR ((triple4 ((triple6 triple2) -> rule3)) -> rule6) OR ((triple4 ((triple6 triple5) -> rule1)) -> rule6) OR ((triple4 ((triple6 ((triple2) -> rule5)) -> rule1)) -> rule6))] Bob is blue.[(triple2 OR ((triple3) -> rule4) OR ((triple1 triple3) -> rule8) OR ((((triple6 triple5) -> rule1)) -> rule4) OR ((triple1 ((triple6 triple5) -> rule1)) -> rule8) OR ((((triple4 triple3) -> rule6) triple3) -> rule8) OR ((((triple4 triple3) -> rule6) ((triple6 triple5) -> rule1)) -> rule8) OR ((((((triple1 triple7) -> rule7) triple5) -> rule1)) -> rule4) OR ((((((triple4 triple1) -> rule2) triple5) -> rule1)) -> rule4) OR ((triple1 ((((triple1 triple7) -> rule7) triple5) -> rule1)) -> rule8) OR ((triple1 ((((triple4 triple1) -> rule2) triple5) -> rule1)) -> rule8) OR ((((triple4 ((triple6 triple5) -> rule1)) -> rule6) triple3) -> rule8) OR ((((triple4 triple3) -> rule6) ((((triple1 triple7) -> rule7) triple5) -> rule1)) -> rule8) OR ((((triple4 triple3) -> rule6) ((((triple4 triple1) -> rule2) triple5) -> rule1)) -> rule8) OR ((((triple4 ((triple6 triple5) -> rule1)) -> rule6) ((triple6 triple5) -> rule1)) -> rule8) OR ((((triple4 ((triple6 triple5) -> rule1)) -> rule6) ((((triple1 triple7) -> rule7) triple5) -> rule1)) -> rule8) OR ((((triple4 ((triple6 triple5) -> rule1)) -> rule6) ((((triple4 triple1) -> rule2) triple5) -> rule1)) -> rule8))] Bob is cold.[(triple3 OR ((triple6 triple2) -> rule3) OR ((triple6 triple5) -> rule1) OR ((triple6 ((triple2) -> rule5)) -> rule1) OR ((((triple1 triple7) -> rule7) triple2) -> rule3) OR ((((triple1 triple7) -> rule7) triple5) -> rule1) OR ((((triple4 triple1) -> rule2) triple2) -> rule3) OR ((((triple4 triple1) -> rule2) triple5) -> rule1) OR ((((triple1 triple7) -> rule7) ((triple2) -> rule5)) -> rule1) OR ((((triple4 triple1) -> rule2) ((triple2) -> rule5)) -> rule1))] Bob is furry.[(triple4)] Bob is red.[(triple5 OR ((triple2) -> rule5) OR ((((triple3) -> rule4)) -> rule5) OR ((((triple1 triple3) -> rule8)) -> rule5) OR ((((((triple4 triple3) -> rule6) triple3) -> rule8)) -> rule5))] Bob is white.[(triple6 OR ((triple1 triple7) -> rule7) OR ((triple4 triple1) -> rule2) OR ((triple4 ((triple4 triple3) -> rule6)) -> rule2) OR ((((triple4 triple3) -> rule6) triple7) -> rule7))] Bob is young.[(triple7)]
Bob is big.
("Bob" "is" "big" "+")
triple1
((triple4 triple3) -> (rule6 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
((triple4 ((triple6 triple2) -> (rule3 % int2))) -> (rule6 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
((triple4 ((triple6 triple5) -> (rule1 % int2))) -> (rule6 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
((triple4 ((triple6 ((triple2) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
Bob is blue.
("Bob" "is" "blue" "+")
triple2
((triple3) -> (rule4 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
((triple1 triple3) -> (rule8 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
((((triple6 triple5) -> (rule1 % int2))) -> (rule4 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
((triple1 ((triple6 triple5) -> (rule1 % int2))) -> (rule8 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
((((triple4 triple3) -> (rule6 % int2)) triple3) -> (rule8 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
((((triple4 triple3) -> (rule6 % int3)) ((triple6 triple5) -> (rule1 % int2))) -> (rule8 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
((((((triple1 triple7) -> (rule7 % int3)) triple5) -> (rule1 % int2))) -> (rule4 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
((((((triple4 triple1) -> (rule2 % int3)) triple5) -> (rule1 % int2))) -> (rule4 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
((triple1 ((((triple1 triple7) -> (rule7 % int3)) triple5) -> (rule1 % int2))) -> (rule8 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
((triple1 ((((triple4 triple1) -> (rule2 % int3)) triple5) -> (rule1 % int2))) -> (rule8 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
((((triple4 ((triple6 triple5) -> (rule1 % int3))) -> (rule6 % int2)) triple3) -> (rule8 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3
((((triple4 triple3) -> (rule6 % int4)) ((((triple1 triple7) -> (rule7 % int3)) triple5) -> (rule1 % int2))) -> (rule8 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is big.
("Bob" "is" "big" "+")
int4
((((triple4 triple3) -> (rule6 % int4)) ((((triple4 triple1) -> (rule2 % int3)) triple5) -> (rule1 % int2))) -> (rule8 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is big.
("Bob" "is" "big" "+")
int4
((((triple4 ((triple6 triple5) -> (rule1 % int3))) -> (rule6 % int2)) ((triple6 triple5) -> (rule1 % int3))) -> (rule8 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3
((((triple4 ((triple6 triple5) -> (rule1 % int4))) -> (rule6 % int3)) ((((triple1 triple7) -> (rule7 % int2)) triple5) -> (rule1 % int4))) -> (rule8 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
Bob is cold.
("Bob" "is" "cold" "+")
int4
((((triple4 ((triple6 triple5) -> (rule1 % int4))) -> (rule6 % int3)) ((((triple4 triple1) -> (rule2 % int2)) triple5) -> (rule1 % int4))) -> (rule8 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
Bob is cold.
("Bob" "is" "cold" "+")
int4
Bob is cold.
("Bob" "is" "cold" "+")
triple3
((triple6 triple2) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
((triple6 triple5) -> (rule1 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
((triple6 ((triple2) -> (rule5 % int2))) -> (rule1 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
((((triple1 triple7) -> (rule7 % int2)) triple2) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
((((triple1 triple7) -> (rule7 % int2)) triple5) -> (rule1 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
((((triple4 triple1) -> (rule2 % int2)) triple2) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
((((triple4 triple1) -> (rule2 % int2)) triple5) -> (rule1 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
((((triple1 triple7) -> (rule7 % int3)) ((triple2) -> (rule5 % int2))) -> (rule1 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
((((triple4 triple1) -> (rule2 % int3)) ((triple2) -> (rule5 % int2))) -> (rule1 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is furry.
("Bob" "is" "furry" "+")
triple4
Bob is red.
("Bob" "is" "red" "+")
triple5
((triple2) -> (rule5 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
((((triple3) -> (rule4 % int2))) -> (rule5 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
((((triple1 triple3) -> (rule8 % int2))) -> (rule5 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
((((((triple4 triple3) -> (rule6 % int3)) triple3) -> (rule8 % int2))) -> (rule5 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
Bob is white.
("Bob" "is" "white" "+")
triple6
((triple1 triple7) -> (rule7 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
((triple4 triple1) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
((triple4 ((triple4 triple3) -> (rule6 % int2))) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
((((triple4 triple3) -> (rule6 % int2)) triple7) -> (rule7 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
triple7