Bob is furry. Charlie is furry. Charlie is quiet. Erin is quiet. Erin is red. Erin is round. Erin is smart. Smart things are red. If something is quiet then it is furry. All quiet things are smart. If something is red and furry then it is white. If Erin is white and Erin is quiet then Erin is smart. If Erin is furry and Erin is red then Erin is round.
Bob is furry.
("Bob" "is" "furry" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is round.
("Erin" "is" "round" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Smart things are red.
((("something" "is" "smart" "+")) -> ("something" "is" "red" "+"))
If something is quiet then it is furry.
((("something" "is" "quiet" "+")) -> ("something" "is" "furry" "+"))
All quiet things are smart.
((("something" "is" "quiet" "+")) -> ("something" "is" "smart" "+"))
If something is red and furry then it is white.
((("something" "is" "red" "+") ("something" "is" "furry" "+")) -> ("something" "is" "white" "+"))
If Erin is white and Erin is quiet then Erin is smart.
((("Erin" "is" "white" "+") ("Erin" "is" "quiet" "+")) -> ("Erin" "is" "smart" "+"))
If Erin is furry and Erin is red then Erin is round.
((("Erin" "is" "furry" "+") ("Erin" "is" "red" "+")) -> ("Erin" "is" "round" "+"))
Erin is round.
True
1
proof
[(triple6 OR ((((triple4) -> rule2) triple5) -> rule6) OR ((((triple4) -> rule2) ((triple7) -> rule1)) -> rule6) OR ((((triple4) -> rule2) ((((triple4) -> rule3)) -> rule1)) -> rule6))]
("Erin" "is" "round" "+")
triple6
((((triple4) -> (rule2 % int2)) triple5) -> (rule6 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
((((triple4) -> (rule2 % int3)) ((triple7) -> (rule1 % int2))) -> (rule6 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
int3
((((triple4) -> (rule2 % int4)) ((((triple4) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Erin is furry.
("Erin" "is" "furry" "+")
int4
Erin is not round.
False
1
inv-proof
[(triple6 OR ((((triple4) -> rule2) triple5) -> rule6) OR ((((triple4) -> rule2) ((triple7) -> rule1)) -> rule6) OR ((((triple4) -> rule2) ((((triple4) -> rule3)) -> rule1)) -> rule6))]
("Erin" "is" "round" "-")
triple6
((((triple4) -> (rule2 % int2)) triple5) -> (rule6 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
((((triple4) -> (rule2 % int3)) ((triple7) -> (rule1 % int2))) -> (rule6 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
int3
((((triple4) -> (rule2 % int4)) ((((triple4) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Erin is furry.
("Erin" "is" "furry" "+")
int4
Charlie is smart.
True
2
proof
[(((triple3) -> rule3))]
("Charlie" "is" "smart" "+")
((triple3) -> (rule3 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Erin is not furry.
False
2
inv-proof
[(((triple4) -> rule2))]
("Erin" "is" "furry" "-")
((triple4) -> (rule2 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is white.
True
4
proof
[(((triple5 ((triple4) -> rule2)) -> rule4) OR ((((triple7) -> rule1) ((triple4) -> rule2)) -> rule4) OR ((((((triple4) -> rule3)) -> rule1) ((triple4) -> rule2)) -> rule4))]
("Erin" "is" "white" "+")
((triple5 ((triple4) -> (rule2 % int2))) -> (rule4 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
((((triple7) -> (rule1 % int3)) ((triple4) -> (rule2 % int2))) -> (rule4 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
((((((triple4) -> (rule3 % int4))) -> (rule1 % int3)) ((triple4) -> (rule2 % int2))) -> (rule4 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
Erin is smart.
("Erin" "is" "smart" "+")
int4
Erin is not white.
False
4
inv-proof
[(((triple5 ((triple4) -> rule2)) -> rule4) OR ((((triple7) -> rule1) ((triple4) -> rule2)) -> rule4) OR ((((((triple4) -> rule3)) -> rule1) ((triple4) -> rule2)) -> rule4))]
("Erin" "is" "white" "-")
((triple5 ((triple4) -> (rule2 % int2))) -> (rule4 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
((((triple7) -> (rule1 % int3)) ((triple4) -> (rule2 % int2))) -> (rule4 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
((((((triple4) -> (rule3 % int4))) -> (rule1 % int3)) ((triple4) -> (rule2 % int2))) -> (rule4 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
Erin is smart.
("Erin" "is" "smart" "+")
int4
Charlie is white.
True
5
proof
[(((((((triple3) -> rule3)) -> rule1) triple2) -> rule4) OR ((((((triple3) -> rule3)) -> rule1) ((triple3) -> rule2)) -> rule4))]
("Charlie" "is" "white" "+")
((((((triple3) -> (rule3 % int3))) -> (rule1 % int2)) triple2) -> (rule4 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
((((((triple3) -> (rule3 % int4))) -> (rule1 % int3)) ((triple3) -> (rule2 % int2))) -> (rule4 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
int3
Charlie is smart.
("Charlie" "is" "smart" "+")
int4
Charlie is not white.
False
5
inv-proof
[(((((((triple3) -> rule3)) -> rule1) triple2) -> rule4) OR ((((((triple3) -> rule3)) -> rule1) ((triple3) -> rule2)) -> rule4))]
("Charlie" "is" "white" "-")
((((((triple3) -> (rule3 % int3))) -> (rule1 % int2)) triple2) -> (rule4 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
((((((triple3) -> (rule3 % int4))) -> (rule1 % int3)) ((triple3) -> (rule2 % int2))) -> (rule4 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
int3
Charlie is smart.
("Charlie" "is" "smart" "+")
int4
Bob is not smart.
Unknown
inv-rconc
[@1: Bob is smart.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Bob" "is" "smart" "-")
Bob is red.
Unknown
rconc
[@2: Bob is red.[CWA. Example of deepest failure = (rule1 <- rule3 <- FAIL)]]
("Bob" "is" "red" "+")
Bob is not white.
Unknown
inv-rconc
[@3: Bob is white.[CWA. Example of deepest failure = (rule4 <- rule1 <- rule3 <- FAIL)]]
("Bob" "is" "white" "-")
Charlie is nice.
Unknown
random
[@0: Charlie is nice.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "nice" "+")
Charlie is not round.
Unknown
inv-random
[@0: Charlie is round.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "round" "-")
Erin is nice.
Unknown
random
[@0: Erin is nice.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "nice" "+")
Bob is not quiet.
Unknown
inv-random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "-")
Bob is nice.
Unknown
random
[@0: Bob is nice.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "nice" "+")
@0: Bob is furry.[(triple1)] Charlie is furry.[(triple2 OR ((triple3) -> rule2))] Charlie is quiet.[(triple3)] Erin is quiet.[(triple4)] Erin is red.[(triple5 OR ((triple7) -> rule1) OR ((((triple4) -> rule3)) -> rule1))] Erin is round.[(triple6 OR ((((triple4) -> rule2) triple5) -> rule6) OR ((((triple4) -> rule2) ((triple7) -> rule1)) -> rule6) OR ((((triple4) -> rule2) ((((triple4) -> rule3)) -> rule1)) -> rule6))] Erin is smart.[(triple7 OR ((triple4) -> rule3) OR ((((triple5 ((triple4) -> rule2)) -> rule4) triple4) -> rule5))] @1: Charlie is smart.[(((triple3) -> rule3))] Erin is furry.[(((triple4) -> rule2))] @2: Charlie is red.[(((((triple3) -> rule3)) -> rule1))] Erin is white.[(((triple5 ((triple4) -> rule2)) -> rule4) OR ((((triple7) -> rule1) ((triple4) -> rule2)) -> rule4) OR ((((((triple4) -> rule3)) -> rule1) ((triple4) -> rule2)) -> rule4))] @3: Charlie is white.[(((((((triple3) -> rule3)) -> rule1) triple2) -> rule4) OR ((((((triple3) -> rule3)) -> rule1) ((triple3) -> rule2)) -> rule4))]
Bob is furry.
("Bob" "is" "furry" "+")
triple1
Charlie is furry.
("Charlie" "is" "furry" "+")
triple2
((triple3) -> (rule2 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple3
Erin is quiet.
("Erin" "is" "quiet" "+")
triple4
Erin is red.
("Erin" "is" "red" "+")
triple5
((triple7) -> (rule1 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
((((triple4) -> (rule3 % int2))) -> (rule1 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
triple6
((((triple4) -> (rule2 % int2)) triple5) -> (rule6 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
((((triple4) -> (rule2 % int3)) ((triple7) -> (rule1 % int2))) -> (rule6 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
int3
((((triple4) -> (rule2 % int4)) ((((triple4) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Erin is furry.
("Erin" "is" "furry" "+")
int4
Erin is smart.
("Erin" "is" "smart" "+")
triple7
((triple4) -> (rule3 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
((((triple5 ((triple4) -> (rule2 % int3))) -> (rule4 % int2)) triple4) -> (rule5 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
int3
Charlie is smart.
("Charlie" "is" "smart" "+")
((triple3) -> (rule3 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
((triple4) -> (rule2 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
((((triple3) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
((triple5 ((triple4) -> (rule2 % int2))) -> (rule4 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
((((triple7) -> (rule1 % int3)) ((triple4) -> (rule2 % int2))) -> (rule4 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
((((((triple4) -> (rule3 % int4))) -> (rule1 % int3)) ((triple4) -> (rule2 % int2))) -> (rule4 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
Erin is smart.
("Erin" "is" "smart" "+")
int4
Charlie is white.
("Charlie" "is" "white" "+")
((((((triple3) -> (rule3 % int3))) -> (rule1 % int2)) triple2) -> (rule4 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
((((((triple3) -> (rule3 % int4))) -> (rule1 % int3)) ((triple3) -> (rule2 % int2))) -> (rule4 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
int3
Charlie is smart.
("Charlie" "is" "smart" "+")
int4