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