Bob is furry. Bob is red. Bob is young. Charlie is big. Charlie is quiet. Charlie is red. Charlie is rough. Charlie is young. Gary is big. Gary is cold. Gary is furry. Gary is quiet. Gary is red. Gary is rough. Gary is young. If someone is red and big then they are furry. All quiet, red people are furry. Quiet, big people are furry. All young, red people are quiet. If Bob is furry then Bob is red. If someone is furry then they are cold. Red people are quiet. Big people are furry.
Bob is furry.
("Bob" "is" "furry" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is young.
("Bob" "is" "young" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is young.
("Gary" "is" "young" "+")
If someone is red and big then they are furry.
((("someone" "is" "red" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "furry" "+"))
All quiet, red people are furry.
((("someone" "is" "quiet" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "furry" "+"))
Quiet, big people are furry.
((("someone" "is" "quiet" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "furry" "+"))
All young, red people are quiet.
((("someone" "is" "young" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "quiet" "+"))
If Bob is furry then Bob is red.
((("Bob" "is" "furry" "+")) -> ("Bob" "is" "red" "+"))
If someone is furry then they are cold.
((("someone" "is" "furry" "+")) -> ("someone" "is" "cold" "+"))
Red people are quiet.
((("someone" "is" "red" "+")) -> ("someone" "is" "quiet" "+"))
Big people are furry.
((("someone" "is" "big" "+")) -> ("someone" "is" "furry" "+"))
Bob is furry.
True
1
proof
[(triple1 OR ((((triple2) -> rule7) triple2) -> rule2) OR ((((triple3 triple2) -> rule4) triple2) -> rule2))]
("Bob" "is" "furry" "+")
triple1
((((triple2) -> (rule7 % int2)) triple2) -> (rule2 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
((((triple3 triple2) -> (rule4 % int2)) triple2) -> (rule2 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Charlie is not quiet.
False
1
inv-proof
[(triple5 OR ((triple6) -> rule7) OR ((triple8 triple6) -> rule4))]
("Charlie" "is" "quiet" "-")
triple5
((triple6) -> (rule7 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
((triple8 triple6) -> (rule4 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is furry.
True
2
proof
[(((triple4) -> rule8) OR ((triple5 triple4) -> rule3) OR ((triple5 triple6) -> rule2) OR ((triple6 triple4) -> rule1) OR ((((triple6) -> rule7) triple4) -> rule3) OR ((((triple6) -> rule7) triple6) -> rule2) OR ((((triple8 triple6) -> rule4) triple4) -> rule3) OR ((((triple8 triple6) -> rule4) triple6) -> rule2))]
("Charlie" "is" "furry" "+")
((triple4) -> (rule8 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
((triple5 triple4) -> (rule3 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
((triple5 triple6) -> (rule2 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
((triple6 triple4) -> (rule1 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
((((triple6) -> (rule7 % int2)) triple4) -> (rule3 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
((((triple6) -> (rule7 % int2)) triple6) -> (rule2 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
((((triple8 triple6) -> (rule4 % int2)) triple4) -> (rule3 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
((((triple8 triple6) -> (rule4 % int2)) triple6) -> (rule2 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is not furry.
False
2
inv-proof
[(((triple4) -> rule8) OR ((triple5 triple4) -> rule3) OR ((triple5 triple6) -> rule2) OR ((triple6 triple4) -> rule1) OR ((((triple6) -> rule7) triple4) -> rule3) OR ((((triple6) -> rule7) triple6) -> rule2) OR ((((triple8 triple6) -> rule4) triple4) -> rule3) OR ((((triple8 triple6) -> rule4) triple6) -> rule2))]
("Charlie" "is" "furry" "-")
((triple4) -> (rule8 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
((triple5 triple4) -> (rule3 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
((triple5 triple6) -> (rule2 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
((triple6 triple4) -> (rule1 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
((((triple6) -> (rule7 % int2)) triple4) -> (rule3 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
((((triple6) -> (rule7 % int2)) triple6) -> (rule2 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
((((triple8 triple6) -> (rule4 % int2)) triple4) -> (rule3 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
((((triple8 triple6) -> (rule4 % int2)) triple6) -> (rule2 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Bob is not rough.
Unknown
inv-random
[@0: Bob is rough.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "rough" "-")
Bob is big.
Unknown
random
[@0: Bob is big.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "big" "+")
@0: Bob is furry.[(triple1 OR ((((triple2) -> rule7) triple2) -> rule2) OR ((((triple3 triple2) -> rule4) triple2) -> rule2))] Bob is red.[(triple2 OR ((triple1) -> rule5))] Bob is young.[(triple3)] Charlie is big.[(triple4)] Charlie is quiet.[(triple5 OR ((triple6) -> rule7) OR ((triple8 triple6) -> rule4))] Charlie is red.[(triple6)] Charlie is rough.[(triple7)] Charlie is young.[(triple8)] Gary is big.[(triple9)] Gary is cold.[(triple10 OR ((triple11) -> rule6) OR ((((triple9) -> rule8)) -> rule6) OR ((((triple12 triple13) -> rule2)) -> rule6) OR ((((triple12 triple9) -> rule3)) -> rule6) OR ((((triple13 triple9) -> rule1)) -> rule6) OR ((((((triple13) -> rule7) triple13) -> rule2)) -> rule6) OR ((((((triple13) -> rule7) triple9) -> rule3)) -> rule6) OR ((((((triple15 triple13) -> rule4) triple13) -> rule2)) -> rule6) OR ((((((triple15 triple13) -> rule4) triple9) -> rule3)) -> rule6))] Gary is furry.[(triple11 OR ((triple9) -> rule8) OR ((triple12 triple13) -> rule2) OR ((triple12 triple9) -> rule3) OR ((triple13 triple9) -> rule1) OR ((((triple13) -> rule7) triple13) -> rule2) OR ((((triple13) -> rule7) triple9) -> rule3) OR ((((triple15 triple13) -> rule4) triple13) -> rule2) OR ((((triple15 triple13) -> rule4) triple9) -> rule3))] Gary is quiet.[(triple12 OR ((triple13) -> rule7) OR ((triple15 triple13) -> rule4))] Gary is red.[(triple13)] Gary is rough.[(triple14)] Gary is young.[(triple15)] @1: Bob is cold.[(((triple1) -> rule6) OR ((((((triple2) -> rule7) triple2) -> rule2)) -> rule6) OR ((((((triple3 triple2) -> rule4) triple2) -> rule2)) -> rule6))] Bob is quiet.[(((triple2) -> rule7) OR ((triple3 triple2) -> rule4) OR ((((triple1) -> rule5)) -> rule7) OR ((triple3 ((triple1) -> rule5)) -> rule4))] Charlie is furry.[(((triple4) -> rule8) OR ((triple5 triple4) -> rule3) OR ((triple5 triple6) -> rule2) OR ((triple6 triple4) -> rule1) OR ((((triple6) -> rule7) triple4) -> rule3) OR ((((triple6) -> rule7) triple6) -> rule2) OR ((((triple8 triple6) -> rule4) triple4) -> rule3) OR ((((triple8 triple6) -> rule4) triple6) -> rule2))] @2: Charlie is cold.[(((((triple4) -> rule8)) -> rule6) OR ((((triple5 triple4) -> rule3)) -> rule6) OR ((((triple5 triple6) -> rule2)) -> rule6) OR ((((triple6 triple4) -> rule1)) -> rule6) OR ((((((triple6) -> rule7) triple4) -> rule3)) -> rule6) OR ((((((triple6) -> rule7) triple6) -> rule2)) -> rule6) OR ((((((triple8 triple6) -> rule4) triple4) -> rule3)) -> rule6) OR ((((((triple8 triple6) -> rule4) triple6) -> rule2)) -> rule6))]
Bob is furry.
("Bob" "is" "furry" "+")
triple1
((((triple2) -> (rule7 % int2)) triple2) -> (rule2 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
((((triple3 triple2) -> (rule4 % int2)) triple2) -> (rule2 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
triple2
((triple1) -> (rule5 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
triple3
Charlie is big.
("Charlie" "is" "big" "+")
triple4
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple5
((triple6) -> (rule7 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
((triple8 triple6) -> (rule4 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
triple6
Charlie is rough.
("Charlie" "is" "rough" "+")
triple7
Charlie is young.
("Charlie" "is" "young" "+")
triple8
Gary is big.
("Gary" "is" "big" "+")
triple9
Gary is cold.
("Gary" "is" "cold" "+")
triple10
((triple11) -> (rule6 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
((((triple9) -> (rule8 % int2))) -> (rule6 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
((((triple12 triple13) -> (rule2 % int2))) -> (rule6 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
((((triple12 triple9) -> (rule3 % int2))) -> (rule6 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
((((triple13 triple9) -> (rule1 % int2))) -> (rule6 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
((((((triple13) -> (rule7 % int3)) triple13) -> (rule2 % int2))) -> (rule6 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
((((((triple13) -> (rule7 % int3)) triple9) -> (rule3 % int2))) -> (rule6 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
((((((triple15 triple13) -> (rule4 % int3)) triple13) -> (rule2 % int2))) -> (rule6 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
((((((triple15 triple13) -> (rule4 % int3)) triple9) -> (rule3 % int2))) -> (rule6 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
Gary is furry.
("Gary" "is" "furry" "+")
triple11
((triple9) -> (rule8 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
((triple12 triple13) -> (rule2 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
((triple12 triple9) -> (rule3 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
((triple13 triple9) -> (rule1 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
((((triple13) -> (rule7 % int2)) triple13) -> (rule2 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
((((triple13) -> (rule7 % int2)) triple9) -> (rule3 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
((((triple15 triple13) -> (rule4 % int2)) triple13) -> (rule2 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
((((triple15 triple13) -> (rule4 % int2)) triple9) -> (rule3 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
triple12
((triple13) -> (rule7 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
((triple15 triple13) -> (rule4 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
triple13
Gary is rough.
("Gary" "is" "rough" "+")
triple14
Gary is young.
("Gary" "is" "young" "+")
triple15
Bob is cold.
("Bob" "is" "cold" "+")
((triple1) -> (rule6 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
((((((triple2) -> (rule7 % int3)) triple2) -> (rule2 % int2))) -> (rule6 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
((((((triple3 triple2) -> (rule4 % int3)) triple2) -> (rule2 % int2))) -> (rule6 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
Bob is quiet.
("Bob" "is" "quiet" "+")
((triple2) -> (rule7 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
((triple3 triple2) -> (rule4 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
((((triple1) -> (rule5 % int2))) -> (rule7 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
((triple3 ((triple1) -> (rule5 % int2))) -> (rule4 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
((triple4) -> (rule8 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
((triple5 triple4) -> (rule3 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
((triple5 triple6) -> (rule2 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
((triple6 triple4) -> (rule1 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
((((triple6) -> (rule7 % int2)) triple4) -> (rule3 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
((((triple6) -> (rule7 % int2)) triple6) -> (rule2 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
((((triple8 triple6) -> (rule4 % int2)) triple4) -> (rule3 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
((((triple8 triple6) -> (rule4 % int2)) triple6) -> (rule2 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
((((triple4) -> (rule8 % int2))) -> (rule6 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
((((triple5 triple4) -> (rule3 % int2))) -> (rule6 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
((((triple5 triple6) -> (rule2 % int2))) -> (rule6 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
((((triple6 triple4) -> (rule1 % int2))) -> (rule6 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
((((((triple6) -> (rule7 % int3)) triple4) -> (rule3 % int2))) -> (rule6 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
((((((triple6) -> (rule7 % int3)) triple6) -> (rule2 % int2))) -> (rule6 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
((((((triple8 triple6) -> (rule4 % int3)) triple4) -> (rule3 % int2))) -> (rule6 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
((((((triple8 triple6) -> (rule4 % int3)) triple6) -> (rule2 % int2))) -> (rule6 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3