Anne is cold. Anne is quiet. Anne is round. Bob is green. Bob is kind. Charlie is furry. Charlie is kind. Charlie is rough. Erin is furry. Erin is green. Erin is quiet. Erin is round. If someone is rough then they are furry. If Erin is round then Erin is furry. Green people are rough. Furry, cold people are rough. Furry, kind people are cold. Quiet people are green.
Anne is cold.
("Anne" "is" "cold" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is round.
("Anne" "is" "round" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is round.
("Erin" "is" "round" "+")
If someone is rough then they are furry.
((("someone" "is" "rough" "+")) -> ("someone" "is" "furry" "+"))
If Erin is round then Erin is furry.
((("Erin" "is" "round" "+")) -> ("Erin" "is" "furry" "+"))
Green people are rough.
((("someone" "is" "green" "+")) -> ("someone" "is" "rough" "+"))
Furry, cold people are rough.
((("someone" "is" "furry" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "rough" "+"))
Furry, kind people are cold.
((("someone" "is" "furry" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "cold" "+"))
Quiet people are green.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "green" "+"))
Anne is cold.
True
1
proof
[(triple1)]
("Anne" "is" "cold" "+")
triple1
Erin is not furry.
False
1
inv-proof
[(triple9 OR ((triple12) -> rule2) OR ((((triple10) -> rule3)) -> rule1) OR ((((((triple11) -> rule6)) -> rule3)) -> rule1))]
("Erin" "is" "furry" "-")
triple9
((triple12) -> (rule2 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
((((triple10) -> (rule3 % int2))) -> (rule1 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
((((((triple11) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
Charlie is cold.
True
3
proof
[(((triple6 triple7) -> rule5) OR ((((triple8) -> rule1) triple7) -> rule5))]
("Charlie" "is" "cold" "+")
((triple6 triple7) -> (rule5 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
((((triple8) -> (rule1 % int2)) triple7) -> (rule5 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is not cold.
False
3
inv-proof
[(((triple6 triple7) -> rule5) OR ((((triple8) -> rule1) triple7) -> rule5))]
("Charlie" "is" "cold" "-")
((triple6 triple7) -> (rule5 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
((((triple8) -> (rule1 % int2)) triple7) -> (rule5 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Bob is furry.
True
3
proof
[(((((triple4) -> rule3)) -> rule1))]
("Bob" "is" "furry" "+")
((((triple4) -> (rule3 % int2))) -> (rule1 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is not furry.
False
3
inv-proof
[(((((triple4) -> rule3)) -> rule1))]
("Bob" "is" "furry" "-")
((((triple4) -> (rule3 % int2))) -> (rule1 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is cold.
True
5
proof
[(((((((triple4) -> rule3)) -> rule1) triple5) -> rule5))]
("Bob" "is" "cold" "+")
((((((triple4) -> (rule3 % int3))) -> (rule1 % int2)) triple5) -> (rule5 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
Bob is not cold.
False
5
inv-proof
[(((((((triple4) -> rule3)) -> rule1) triple5) -> rule5))]
("Bob" "is" "cold" "-")
((((((triple4) -> (rule3 % int3))) -> (rule1 % int2)) triple5) -> (rule5 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
Charlie is not green.
Unknown
inv-rconc
[@1: Charlie is green.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Charlie" "is" "green" "-")
Erin is cold.
Unknown
rconc
[@1: Erin is cold.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Erin" "is" "cold" "+")
Bob is not round.
Unknown
inv-random
[@0: Bob is round.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "round" "-")
Charlie is round.
Unknown
random
[@0: Charlie is round.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "round" "+")
Bob is not quiet.
Unknown
inv-random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "-")
Anne is kind.
Unknown
random
[@0: Anne is kind.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "kind" "+")
Charlie is not quiet.
Unknown
inv-random
[@0: Charlie is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "quiet" "-")
Erin is kind.
Unknown
random
[@0: Erin is kind.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "kind" "+")
@0: Anne is cold.[(triple1)] Anne is quiet.[(triple2)] Anne is round.[(triple3)] Bob is green.[(triple4)] Bob is kind.[(triple5)] Charlie is furry.[(triple6 OR ((triple8) -> rule1))] Charlie is kind.[(triple7)] Charlie is rough.[(triple8 OR ((triple6 ((triple6 triple7) -> rule5)) -> rule4))] Erin is furry.[(triple9 OR ((triple12) -> rule2) OR ((((triple10) -> rule3)) -> rule1) OR ((((((triple11) -> rule6)) -> rule3)) -> rule1))] Erin is green.[(triple10 OR ((triple11) -> rule6))] Erin is quiet.[(triple11)] Erin is round.[(triple12)] @1: Anne is green.[(((triple2) -> rule6))] Bob is rough.[(((triple4) -> rule3))] Charlie is cold.[(((triple6 triple7) -> rule5) OR ((((triple8) -> rule1) triple7) -> rule5))] Erin is rough.[(((triple10) -> rule3) OR ((((triple11) -> rule6)) -> rule3))] @2: Anne is rough.[(((((triple2) -> rule6)) -> rule3))] Bob is furry.[(((((triple4) -> rule3)) -> rule1))] @3: Anne is furry.[(((((((triple2) -> rule6)) -> rule3)) -> rule1))] Bob is cold.[(((((((triple4) -> rule3)) -> rule1) triple5) -> rule5))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Anne is quiet.
("Anne" "is" "quiet" "+")
triple2
Anne is round.
("Anne" "is" "round" "+")
triple3
Bob is green.
("Bob" "is" "green" "+")
triple4
Bob is kind.
("Bob" "is" "kind" "+")
triple5
Charlie is furry.
("Charlie" "is" "furry" "+")
triple6
((triple8) -> (rule1 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
triple7
Charlie is rough.
("Charlie" "is" "rough" "+")
triple8
((triple6 ((triple6 triple7) -> (rule5 % int2))) -> (rule4 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
triple9
((triple12) -> (rule2 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
((((triple10) -> (rule3 % int2))) -> (rule1 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
((((((triple11) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
Erin is green.
("Erin" "is" "green" "+")
triple10
((triple11) -> (rule6 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
triple11
Erin is round.
("Erin" "is" "round" "+")
triple12
Anne is green.
("Anne" "is" "green" "+")
((triple2) -> (rule6 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
((triple4) -> (rule3 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
((triple6 triple7) -> (rule5 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
((((triple8) -> (rule1 % int2)) triple7) -> (rule5 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
((triple10) -> (rule3 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
((((triple11) -> (rule6 % int2))) -> (rule3 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
((((triple2) -> (rule6 % int2))) -> (rule3 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
((((triple4) -> (rule3 % int2))) -> (rule1 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
((((((triple2) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
Bob is cold.
("Bob" "is" "cold" "+")
((((((triple4) -> (rule3 % int3))) -> (rule1 % int2)) triple5) -> (rule5 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3