Dave is big. Dave is cold. Dave is furry. Dave is kind. Dave is rough. Dave is smart. Dave is white. Erin is cold. Erin is furry. Erin is kind. Erin is smart. Erin is white. If someone is furry and cold then they are white. If Erin is furry then Erin is white. If someone is kind and smart then they are rough. If Erin is big then Erin is kind. All furry people are rough. If someone is white then they are cold. All furry, white people are big. Big, cold people are white.
Dave is big.
("Dave" "is" "big" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is white.
("Dave" "is" "white" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Erin is white.
("Erin" "is" "white" "+")
If someone is furry and cold then they are white.
((("someone" "is" "furry" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "white" "+"))
If Erin is furry then Erin is white.
((("Erin" "is" "furry" "+")) -> ("Erin" "is" "white" "+"))
If someone is kind and smart then they are rough.
((("someone" "is" "kind" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "rough" "+"))
If Erin is big then Erin is kind.
((("Erin" "is" "big" "+")) -> ("Erin" "is" "kind" "+"))
All furry people are rough.
((("someone" "is" "furry" "+")) -> ("someone" "is" "rough" "+"))
If someone is white then they are cold.
((("someone" "is" "white" "+")) -> ("someone" "is" "cold" "+"))
All furry, white people are big.
((("someone" "is" "furry" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "big" "+"))
Big, cold people are white.
((("someone" "is" "big" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "white" "+"))
Dave is kind.
True
1
proof
[(triple4)]
("Dave" "is" "kind" "+")
triple4
Erin is not cold.
False
1
inv-proof
[(triple8 OR ((triple12) -> rule6) OR ((((triple9) -> rule2)) -> rule6))]
("Erin" "is" "cold" "-")
triple8
((triple12) -> (rule6 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
((((triple9) -> (rule2 % int2))) -> (rule6 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
@0: Dave is big.[(triple1 OR ((triple3 triple7) -> rule7) OR ((triple3 ((triple3 triple2) -> rule1)) -> rule7))] Dave is cold.[(triple2 OR ((triple7) -> rule6))] Dave is furry.[(triple3)] Dave is kind.[(triple4)] Dave is rough.[(triple5 OR ((triple3) -> rule5) OR ((triple4 triple6) -> rule3))] Dave is smart.[(triple6)] Dave is white.[(triple7 OR ((triple1 triple2) -> rule8) OR ((triple3 triple2) -> rule1))] Erin is cold.[(triple8 OR ((triple12) -> rule6) OR ((((triple9) -> rule2)) -> rule6))] Erin is furry.[(triple9)] Erin is kind.[(triple10 OR ((((triple9 triple12) -> rule7)) -> rule4) OR ((((triple9 ((triple9) -> rule2)) -> rule7)) -> rule4) OR ((((triple9 ((triple9 triple8) -> rule1)) -> rule7)) -> rule4))] Erin is smart.[(triple11)] Erin is white.[(triple12 OR ((triple9) -> rule2) OR ((triple9 triple8) -> rule1))] @1: Erin is big.[(((triple9 triple12) -> rule7) OR ((triple9 ((triple9) -> rule2)) -> rule7) OR ((triple9 ((triple9 triple8) -> rule1)) -> rule7))] Erin is rough.[(((triple9) -> rule5) OR ((triple10 triple11) -> rule3) OR ((((((triple9 triple12) -> rule7)) -> rule4) triple11) -> rule3) OR ((((((triple9 ((triple9) -> rule2)) -> rule7)) -> rule4) triple11) -> rule3) OR ((((((triple9 ((triple9 triple8) -> rule1)) -> rule7)) -> rule4) triple11) -> rule3))]
Dave is big.
("Dave" "is" "big" "+")
triple1
((triple3 triple7) -> (rule7 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
((triple3 ((triple3 triple2) -> (rule1 % int2))) -> (rule7 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
triple2
((triple7) -> (rule6 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
triple3
Dave is kind.
("Dave" "is" "kind" "+")
triple4
Dave is rough.
("Dave" "is" "rough" "+")
triple5
((triple3) -> (rule5 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
((triple4 triple6) -> (rule3 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
triple6
Dave is white.
("Dave" "is" "white" "+")
triple7
((triple1 triple2) -> (rule8 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
((triple3 triple2) -> (rule1 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
triple8
((triple12) -> (rule6 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
((((triple9) -> (rule2 % int2))) -> (rule6 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
triple9
Erin is kind.
("Erin" "is" "kind" "+")
triple10
((((triple9 triple12) -> (rule7 % int2))) -> (rule4 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
((((triple9 ((triple9) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
int3
((((triple9 ((triple9 triple8) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
int3
Erin is smart.
("Erin" "is" "smart" "+")
triple11
Erin is white.
("Erin" "is" "white" "+")
triple12
((triple9) -> (rule2 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
((triple9 triple8) -> (rule1 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
((triple9 triple12) -> (rule7 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
((triple9 ((triple9) -> (rule2 % int2))) -> (rule7 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
((triple9 ((triple9 triple8) -> (rule1 % int2))) -> (rule7 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
((triple9) -> (rule5 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
((triple10 triple11) -> (rule3 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
((((((triple9 triple12) -> (rule7 % int3))) -> (rule4 % int2)) triple11) -> (rule3 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3
((((((triple9 ((triple9) -> (rule2 % int4))) -> (rule7 % int3))) -> (rule4 % int2)) triple11) -> (rule3 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3
Erin is white.
("Erin" "is" "white" "+")
int4
((((((triple9 ((triple9 triple8) -> (rule1 % int4))) -> (rule7 % int3))) -> (rule4 % int2)) triple11) -> (rule3 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3
Erin is white.
("Erin" "is" "white" "+")
int4