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