Anne is furry. Bob is blue. Bob is green. Bob is quiet. Bob is red. Erin is big. Erin is nice. Gary is big. Gary is blue. Gary is furry. Gary is green. Gary is nice. Gary is quiet. Gary is red. All nice, quiet people are green. If someone is quiet then they are red. Blue people are furry. Big people are blue. If Erin is green and Erin is big then Erin is quiet. All quiet, big people are red. If Bob is big and Bob is furry then Bob is blue. Furry people are green.
Anne is furry.
("Anne" "is" "furry" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is red.
("Bob" "is" "red" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is red.
("Gary" "is" "red" "+")
All nice, quiet people are green.
((("someone" "is" "nice" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "green" "+"))
If someone is quiet then they are red.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "red" "+"))
Blue people are furry.
((("someone" "is" "blue" "+")) -> ("someone" "is" "furry" "+"))
Big people are blue.
((("someone" "is" "big" "+")) -> ("someone" "is" "blue" "+"))
If Erin is green and Erin is big then Erin is quiet.
((("Erin" "is" "green" "+") ("Erin" "is" "big" "+")) -> ("Erin" "is" "quiet" "+"))
All quiet, big people are red.
((("someone" "is" "quiet" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "red" "+"))
If Bob is big and Bob is furry then Bob is blue.
((("Bob" "is" "big" "+") ("Bob" "is" "furry" "+")) -> ("Bob" "is" "blue" "+"))
Furry people are green.
((("someone" "is" "furry" "+")) -> ("someone" "is" "green" "+"))
Gary is furry.
True
1
proof
[(triple10 OR ((triple9) -> rule3) OR ((((triple8) -> rule4)) -> rule3))]
("Gary" "is" "furry" "+")
triple10
((triple9) -> (rule3 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
((((triple8) -> (rule4 % int2))) -> (rule3 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Bob is not quiet.
False
1
inv-proof
[(triple4)]
("Bob" "is" "quiet" "-")
triple4
Erin is blue.
True
2
proof
[(((triple6) -> rule4))]
("Erin" "is" "blue" "+")
((triple6) -> (rule4 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Bob is not furry.
False
2
inv-proof
[(((triple2) -> rule3))]
("Bob" "is" "furry" "-")
((triple2) -> (rule3 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Erin is furry.
True
3
proof
[(((((triple6) -> rule4)) -> rule3))]
("Erin" "is" "furry" "+")
((((triple6) -> (rule4 % int2))) -> (rule3 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is not furry.
False
3
inv-proof
[(((((triple6) -> rule4)) -> rule3))]
("Erin" "is" "furry" "-")
((((triple6) -> (rule4 % int2))) -> (rule3 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is green.
True
4
proof
[(((((((triple6) -> rule4)) -> rule3)) -> rule8))]
("Erin" "is" "green" "+")
((((((triple6) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3
Erin is not green.
False
4
inv-proof
[(((((((triple6) -> rule4)) -> rule3)) -> rule8))]
("Erin" "is" "green" "-")
((((((triple6) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3
Erin is quiet.
True
6
proof
[(((((((((triple6) -> rule4)) -> rule3)) -> rule8) triple6) -> rule5))]
("Erin" "is" "quiet" "+")
((((((((triple6) -> (rule4 % int4))) -> (rule3 % int3))) -> (rule8 % int2)) triple6) -> (rule5 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
int3
Erin is blue.
("Erin" "is" "blue" "+")
int4
Erin is not quiet.
False
6
inv-proof
[(((((((((triple6) -> rule4)) -> rule3)) -> rule8) triple6) -> rule5))]
("Erin" "is" "quiet" "-")
((((((((triple6) -> (rule4 % int4))) -> (rule3 % int3))) -> (rule8 % int2)) triple6) -> (rule5 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
int3
Erin is blue.
("Erin" "is" "blue" "+")
int4
Erin is red.
True
7
proof
[(((((((((((triple6) -> rule4)) -> rule3)) -> rule8) triple6) -> rule5)) -> rule2) OR ((((((((((triple6) -> rule4)) -> rule3)) -> rule8) triple6) -> rule5) triple6) -> rule6))]
("Erin" "is" "red" "+")
((((((((((triple6) -> (rule4 % int5))) -> (rule3 % int4))) -> (rule8 % int3)) triple6) -> (rule5 % int2))) -> (rule2 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
Erin is furry.
("Erin" "is" "furry" "+")
int4
Erin is blue.
("Erin" "is" "blue" "+")
int5
((((((((((triple6) -> (rule4 % int5))) -> (rule3 % int4))) -> (rule8 % int3)) triple6) -> (rule5 % int2)) triple6) -> (rule6 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
Erin is furry.
("Erin" "is" "furry" "+")
int4
Erin is blue.
("Erin" "is" "blue" "+")
int5
Erin is not red.
False
7
inv-proof
[(((((((((((triple6) -> rule4)) -> rule3)) -> rule8) triple6) -> rule5)) -> rule2) OR ((((((((((triple6) -> rule4)) -> rule3)) -> rule8) triple6) -> rule5) triple6) -> rule6))]
("Erin" "is" "red" "-")
((((((((((triple6) -> (rule4 % int5))) -> (rule3 % int4))) -> (rule8 % int3)) triple6) -> (rule5 % int2))) -> (rule2 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
Erin is furry.
("Erin" "is" "furry" "+")
int4
Erin is blue.
("Erin" "is" "blue" "+")
int5
((((((((((triple6) -> (rule4 % int5))) -> (rule3 % int4))) -> (rule8 % int3)) triple6) -> (rule5 % int2)) triple6) -> (rule6 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
Erin is furry.
("Erin" "is" "furry" "+")
int4
Erin is blue.
("Erin" "is" "blue" "+")
int5
Anne is not red.
Unknown
inv-rconc
[@1: Anne is red.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Anne" "is" "red" "-")
Anne is blue.
Unknown
rconc
[@1: Anne is blue.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Anne" "is" "blue" "+")
Bob is not nice.
Unknown
inv-random
[@0: Bob is nice.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "nice" "-")
Anne is nice.
Unknown
random
[@0: Anne is nice.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "nice" "+")
Bob is not big.
Unknown
inv-random
[@0: Bob is big.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "big" "-")
Anne is quiet.
Unknown
random
[@0: Anne is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "quiet" "+")
@0: Anne is furry.[(triple1)] Bob is blue.[(triple2)] Bob is green.[(triple3 OR ((((triple2) -> rule3)) -> rule8))] Bob is quiet.[(triple4)] Bob is red.[(triple5 OR ((triple4) -> rule2))] Erin is big.[(triple6)] Erin is nice.[(triple7)] Gary is big.[(triple8)] Gary is blue.[(triple9 OR ((triple8) -> rule4))] Gary is furry.[(triple10 OR ((triple9) -> rule3) OR ((((triple8) -> rule4)) -> rule3))] Gary is green.[(triple11 OR ((triple10) -> rule8) OR ((triple12 triple13) -> rule1) OR ((((triple9) -> rule3)) -> rule8) OR ((((((triple8) -> rule4)) -> rule3)) -> rule8))] Gary is nice.[(triple12)] Gary is quiet.[(triple13)] Gary is red.[(triple14 OR ((triple13) -> rule2) OR ((triple13 triple8) -> rule6))] @1: Anne is green.[(((triple1) -> rule8))] Bob is furry.[(((triple2) -> rule3))] Erin is blue.[(((triple6) -> rule4))] @2: Erin is furry.[(((((triple6) -> rule4)) -> rule3))] @3: Erin is green.[(((((((triple6) -> rule4)) -> rule3)) -> rule8))] @4: Erin is quiet.[(((((((((triple6) -> rule4)) -> rule3)) -> rule8) triple6) -> rule5))] @5: Erin is red.[(((((((((((triple6) -> rule4)) -> rule3)) -> rule8) triple6) -> rule5)) -> rule2) OR ((((((((((triple6) -> rule4)) -> rule3)) -> rule8) triple6) -> rule5) triple6) -> rule6))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
Bob is blue.
("Bob" "is" "blue" "+")
triple2
Bob is green.
("Bob" "is" "green" "+")
triple3
((((triple2) -> (rule3 % int2))) -> (rule8 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
triple4
Bob is red.
("Bob" "is" "red" "+")
triple5
((triple4) -> (rule2 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
triple6
Erin is nice.
("Erin" "is" "nice" "+")
triple7
Gary is big.
("Gary" "is" "big" "+")
triple8
Gary is blue.
("Gary" "is" "blue" "+")
triple9
((triple8) -> (rule4 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
triple10
((triple9) -> (rule3 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
((((triple8) -> (rule4 % int2))) -> (rule3 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
triple11
((triple10) -> (rule8 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
((triple12 triple13) -> (rule1 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
((((triple9) -> (rule3 % int2))) -> (rule8 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
((((((triple8) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3
Gary is nice.
("Gary" "is" "nice" "+")
triple12
Gary is quiet.
("Gary" "is" "quiet" "+")
triple13
Gary is red.
("Gary" "is" "red" "+")
triple14
((triple13) -> (rule2 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
((triple13 triple8) -> (rule6 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
((triple1) -> (rule8 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
((triple2) -> (rule3 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
((triple6) -> (rule4 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
((((triple6) -> (rule4 % int2))) -> (rule3 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
((((((triple6) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3
Erin is quiet.
("Erin" "is" "quiet" "+")
((((((((triple6) -> (rule4 % int4))) -> (rule3 % int3))) -> (rule8 % int2)) triple6) -> (rule5 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
int3
Erin is blue.
("Erin" "is" "blue" "+")
int4
Erin is red.
("Erin" "is" "red" "+")
((((((((((triple6) -> (rule4 % int5))) -> (rule3 % int4))) -> (rule8 % int3)) triple6) -> (rule5 % int2))) -> (rule2 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
Erin is furry.
("Erin" "is" "furry" "+")
int4
Erin is blue.
("Erin" "is" "blue" "+")
int5
((((((((((triple6) -> (rule4 % int5))) -> (rule3 % int4))) -> (rule8 % int3)) triple6) -> (rule5 % int2)) triple6) -> (rule6 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
Erin is furry.
("Erin" "is" "furry" "+")
int4
Erin is blue.
("Erin" "is" "blue" "+")
int5