Bob is big. Bob is blue. Bob is cold. Bob is kind. Bob is nice. Bob is round. Bob is smart. Dave is big. Dave is blue. Dave is nice. Dave is round. Dave is smart. If someone is kind and smart then they are cold. Blue people are nice. All cold, smart people are kind. If someone is smart and round then they are kind. If someone is smart then they are kind. Blue, kind people are cold. Smart, cold people are round. If Dave is smart and Dave is nice then Dave is round.
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 nice.
("Bob" "is" "nice" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is smart.
("Dave" "is" "smart" "+")
If someone is kind and smart then they are cold.
((("someone" "is" "kind" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "cold" "+"))
Blue people are nice.
((("someone" "is" "blue" "+")) -> ("someone" "is" "nice" "+"))
All cold, smart people are kind.
((("someone" "is" "cold" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "kind" "+"))
If someone is smart and round then they are kind.
((("someone" "is" "smart" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "kind" "+"))
If someone is smart then they are kind.
((("someone" "is" "smart" "+")) -> ("someone" "is" "kind" "+"))
Blue, kind people are cold.
((("someone" "is" "blue" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "cold" "+"))
Smart, cold people are round.
((("someone" "is" "smart" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "round" "+"))
If Dave is smart and Dave is nice then Dave is round.
((("Dave" "is" "smart" "+") ("Dave" "is" "nice" "+")) -> ("Dave" "is" "round" "+"))
Dave is smart.
True
1
proof
[(triple12)]
("Dave" "is" "smart" "+")
triple12
Bob is not blue.
False
1
inv-proof
[(triple2)]
("Bob" "is" "blue" "-")
triple2
Dave is kind.
True
2
proof
[(((triple12) -> rule5) OR ((triple12 triple11) -> rule4) OR ((triple12 ((triple12 triple10) -> rule8)) -> rule4) OR ((triple12 ((triple12 ((triple9) -> rule2)) -> rule8)) -> rule4))]
("Dave" "is" "kind" "+")
((triple12) -> (rule5 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
((triple12 triple11) -> (rule4 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
((triple12 ((triple12 triple10) -> (rule8 % int2))) -> (rule4 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
((triple12 ((triple12 ((triple9) -> (rule2 % int3))) -> (rule8 % int2))) -> (rule4 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Dave is not kind.
False
2
inv-proof
[(((triple12) -> rule5) OR ((triple12 triple11) -> rule4) OR ((triple12 ((triple12 triple10) -> rule8)) -> rule4) OR ((triple12 ((triple12 ((triple9) -> rule2)) -> rule8)) -> rule4))]
("Dave" "is" "kind" "-")
((triple12) -> (rule5 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
((triple12 triple11) -> (rule4 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
((triple12 ((triple12 triple10) -> (rule8 % int2))) -> (rule4 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
((triple12 ((triple12 ((triple9) -> (rule2 % int3))) -> (rule8 % int2))) -> (rule4 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Dave is cold.
True
4
proof
[(((triple9 ((triple12) -> rule5)) -> rule6) OR ((triple9 ((triple12 triple11) -> rule4)) -> rule6) OR ((((triple12) -> rule5) triple12) -> rule1) OR ((((triple12 triple11) -> rule4) triple12) -> rule1) OR ((triple9 ((triple12 ((triple12 triple10) -> rule8)) -> rule4)) -> rule6) OR ((((triple12 ((triple12 triple10) -> rule8)) -> rule4) triple12) -> rule1) OR ((triple9 ((triple12 ((triple12 ((triple9) -> rule2)) -> rule8)) -> rule4)) -> rule6) OR ((((triple12 ((triple12 ((triple9) -> rule2)) -> rule8)) -> rule4) triple12) -> rule1))]
("Dave" "is" "cold" "+")
((triple9 ((triple12) -> (rule5 % int2))) -> (rule6 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
((triple9 ((triple12 triple11) -> (rule4 % int2))) -> (rule6 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
((((triple12) -> (rule5 % int2)) triple12) -> (rule1 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
((((triple12 triple11) -> (rule4 % int2)) triple12) -> (rule1 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
((triple9 ((triple12 ((triple12 triple10) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
((((triple12 ((triple12 triple10) -> (rule8 % int3))) -> (rule4 % int2)) triple12) -> (rule1 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
((triple9 ((triple12 ((triple12 ((triple9) -> (rule2 % int4))) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Dave is nice.
("Dave" "is" "nice" "+")
int4
((((triple12 ((triple12 ((triple9) -> (rule2 % int4))) -> (rule8 % int3))) -> (rule4 % int2)) triple12) -> (rule1 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Dave is nice.
("Dave" "is" "nice" "+")
int4
Dave is not cold.
False
4
inv-proof
[(((triple9 ((triple12) -> rule5)) -> rule6) OR ((triple9 ((triple12 triple11) -> rule4)) -> rule6) OR ((((triple12) -> rule5) triple12) -> rule1) OR ((((triple12 triple11) -> rule4) triple12) -> rule1) OR ((triple9 ((triple12 ((triple12 triple10) -> rule8)) -> rule4)) -> rule6) OR ((((triple12 ((triple12 triple10) -> rule8)) -> rule4) triple12) -> rule1) OR ((triple9 ((triple12 ((triple12 ((triple9) -> rule2)) -> rule8)) -> rule4)) -> rule6) OR ((((triple12 ((triple12 ((triple9) -> rule2)) -> rule8)) -> rule4) triple12) -> rule1))]
("Dave" "is" "cold" "-")
((triple9 ((triple12) -> (rule5 % int2))) -> (rule6 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
((triple9 ((triple12 triple11) -> (rule4 % int2))) -> (rule6 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
((((triple12) -> (rule5 % int2)) triple12) -> (rule1 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
((((triple12 triple11) -> (rule4 % int2)) triple12) -> (rule1 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
((triple9 ((triple12 ((triple12 triple10) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
((((triple12 ((triple12 triple10) -> (rule8 % int3))) -> (rule4 % int2)) triple12) -> (rule1 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
((triple9 ((triple12 ((triple12 ((triple9) -> (rule2 % int4))) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Dave is nice.
("Dave" "is" "nice" "+")
int4
((((triple12 ((triple12 ((triple9) -> (rule2 % int4))) -> (rule8 % int3))) -> (rule4 % int2)) triple12) -> (rule1 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Dave is nice.
("Dave" "is" "nice" "+")
int4
@0: Bob is big.[(triple1)] Bob is blue.[(triple2)] Bob is cold.[(triple3 OR ((triple2 triple4) -> rule6) OR ((triple4 triple7) -> rule1) OR ((triple2 ((triple7) -> rule5)) -> rule6) OR ((triple2 ((triple7 triple6) -> rule4)) -> rule6) OR ((((triple7) -> rule5) triple7) -> rule1) OR ((((triple7 triple6) -> rule4) triple7) -> rule1))] Bob is kind.[(triple4 OR ((triple7) -> rule5) OR ((triple3 triple7) -> rule3) OR ((triple7 triple6) -> rule4) OR ((triple7 ((triple7 triple3) -> rule7)) -> rule4))] Bob is nice.[(triple5 OR ((triple2) -> rule2))] Bob is round.[(triple6 OR ((triple7 triple3) -> rule7) OR ((triple7 ((triple2 triple4) -> rule6)) -> rule7) OR ((triple7 ((triple4 triple7) -> rule1)) -> rule7) OR ((triple7 ((triple2 ((triple7) -> rule5)) -> rule6)) -> rule7) OR ((triple7 ((((triple7) -> rule5) triple7) -> rule1)) -> rule7))] Bob is smart.[(triple7)] Dave is big.[(triple8)] Dave is blue.[(triple9)] Dave is nice.[(triple10 OR ((triple9) -> rule2))] Dave is round.[(triple11 OR ((triple12 triple10) -> rule8) OR ((triple12 ((triple9) -> rule2)) -> rule8) OR ((triple12 ((triple9 ((triple12) -> rule5)) -> rule6)) -> rule7) OR ((triple12 ((((triple12) -> rule5) triple12) -> rule1)) -> rule7))] Dave is smart.[(triple12)] @1: Dave is kind.[(((triple12) -> rule5) OR ((triple12 triple11) -> rule4) OR ((triple12 ((triple12 triple10) -> rule8)) -> rule4) OR ((triple12 ((triple12 ((triple9) -> rule2)) -> rule8)) -> rule4))] @2: Dave is cold.[(((triple9 ((triple12) -> rule5)) -> rule6) OR ((triple9 ((triple12 triple11) -> rule4)) -> rule6) OR ((((triple12) -> rule5) triple12) -> rule1) OR ((((triple12 triple11) -> rule4) triple12) -> rule1) OR ((triple9 ((triple12 ((triple12 triple10) -> rule8)) -> rule4)) -> rule6) OR ((((triple12 ((triple12 triple10) -> rule8)) -> rule4) triple12) -> rule1) OR ((triple9 ((triple12 ((triple12 ((triple9) -> rule2)) -> rule8)) -> rule4)) -> rule6) OR ((((triple12 ((triple12 ((triple9) -> rule2)) -> rule8)) -> rule4) triple12) -> rule1))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is blue.
("Bob" "is" "blue" "+")
triple2
Bob is cold.
("Bob" "is" "cold" "+")
triple3
((triple2 triple4) -> (rule6 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
((triple4 triple7) -> (rule1 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
((triple2 ((triple7) -> (rule5 % int2))) -> (rule6 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
((triple2 ((triple7 triple6) -> (rule4 % int2))) -> (rule6 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
((((triple7) -> (rule5 % int2)) triple7) -> (rule1 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
((((triple7 triple6) -> (rule4 % int2)) triple7) -> (rule1 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
triple4
((triple7) -> (rule5 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
((triple3 triple7) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
((triple7 triple6) -> (rule4 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
((triple7 ((triple7 triple3) -> (rule7 % int2))) -> (rule4 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
triple5
((triple2) -> (rule2 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
triple6
((triple7 triple3) -> (rule7 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
((triple7 ((triple2 triple4) -> (rule6 % int2))) -> (rule7 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
((triple7 ((triple4 triple7) -> (rule1 % int2))) -> (rule7 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
((triple7 ((triple2 ((triple7) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
((triple7 ((((triple7) -> (rule5 % int3)) triple7) -> (rule1 % int2))) -> (rule7 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
Bob is smart.
("Bob" "is" "smart" "+")
triple7
Dave is big.
("Dave" "is" "big" "+")
triple8
Dave is blue.
("Dave" "is" "blue" "+")
triple9
Dave is nice.
("Dave" "is" "nice" "+")
triple10
((triple9) -> (rule2 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
triple11
((triple12 triple10) -> (rule8 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
((triple12 ((triple9) -> (rule2 % int2))) -> (rule8 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
((triple12 ((triple9 ((triple12) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
((triple12 ((((triple12) -> (rule5 % int3)) triple12) -> (rule1 % int2))) -> (rule7 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
Dave is smart.
("Dave" "is" "smart" "+")
triple12
Dave is kind.
("Dave" "is" "kind" "+")
((triple12) -> (rule5 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
((triple12 triple11) -> (rule4 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
((triple12 ((triple12 triple10) -> (rule8 % int2))) -> (rule4 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
((triple12 ((triple12 ((triple9) -> (rule2 % int3))) -> (rule8 % int2))) -> (rule4 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Dave is cold.
("Dave" "is" "cold" "+")
((triple9 ((triple12) -> (rule5 % int2))) -> (rule6 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
((triple9 ((triple12 triple11) -> (rule4 % int2))) -> (rule6 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
((((triple12) -> (rule5 % int2)) triple12) -> (rule1 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
((((triple12 triple11) -> (rule4 % int2)) triple12) -> (rule1 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
((triple9 ((triple12 ((triple12 triple10) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
((((triple12 ((triple12 triple10) -> (rule8 % int3))) -> (rule4 % int2)) triple12) -> (rule1 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
((triple9 ((triple12 ((triple12 ((triple9) -> (rule2 % int4))) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Dave is nice.
("Dave" "is" "nice" "+")
int4
((((triple12 ((triple12 ((triple9) -> (rule2 % int4))) -> (rule8 % int3))) -> (rule4 % int2)) triple12) -> (rule1 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Dave is nice.
("Dave" "is" "nice" "+")
int4