Anne is big. Anne is furry. Anne is quiet. Anne is red. Anne is white. Erin is furry. Erin is round. Erin is white. Gary is cold. Gary is furry. Gary is red. Gary is round. All big things are quiet. Round things are big. Furry, round things are big. All cold things are big. Red, cold things are furry. Big, red things are cold.
Anne is big.
("Anne" "is" "big" "+")
Anne is furry.
("Anne" "is" "furry" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is white.
("Anne" "is" "white" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is round.
("Erin" "is" "round" "+")
Erin is white.
("Erin" "is" "white" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is round.
("Gary" "is" "round" "+")
All big things are quiet.
((("something" "is" "big" "+")) -> ("something" "is" "quiet" "+"))
Round things are big.
((("something" "is" "round" "+")) -> ("something" "is" "big" "+"))
Furry, round things are big.
((("something" "is" "furry" "+") ("something" "is" "round" "+")) -> ("something" "is" "big" "+"))
All cold things are big.
((("something" "is" "cold" "+")) -> ("something" "is" "big" "+"))
Red, cold things are furry.
((("something" "is" "red" "+") ("something" "is" "cold" "+")) -> ("something" "is" "furry" "+"))
Big, red things are cold.
((("something" "is" "big" "+") ("something" "is" "red" "+")) -> ("something" "is" "cold" "+"))
Erin is white.
True
1
proof
[(triple8)]
("Erin" "is" "white" "+")
triple8
Erin is not white.
False
1
inv-proof
[(triple8)]
("Erin" "is" "white" "-")
triple8
Erin is big.
True
2
proof
[(((triple7) -> rule2) OR ((triple6 triple7) -> rule3))]
("Erin" "is" "big" "+")
((triple7) -> (rule2 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
((triple6 triple7) -> (rule3 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is not big.
False
2
inv-proof
[(((triple7) -> rule2) OR ((triple6 triple7) -> rule3))]
("Erin" "is" "big" "-")
((triple7) -> (rule2 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
((triple6 triple7) -> (rule3 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is not cold.
Unknown
inv-rconc
[@1: Erin is cold.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Erin" "is" "cold" "-")
Gary is white.
Unknown
random
[@0: Gary is white.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "white" "+")
Anne is not round.
Unknown
inv-random
[@0: Anne is round.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "round" "-")
Erin is red.
Unknown
random
[@0: Erin is red.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "red" "+")
@0: Anne is big.[(triple1)] Anne is furry.[(triple2 OR ((triple4 ((triple1 triple4) -> rule6)) -> rule5))] Anne is quiet.[(triple3 OR ((triple1) -> rule1))] Anne is red.[(triple4)] Anne is white.[(triple5)] Erin is furry.[(triple6)] Erin is round.[(triple7)] Erin is white.[(triple8)] Gary is cold.[(triple9 OR ((((triple12) -> rule2) triple11) -> rule6) OR ((((triple10 triple12) -> rule3) triple11) -> rule6))] Gary is furry.[(triple10 OR ((triple11 triple9) -> rule5) OR ((triple11 ((((triple12) -> rule2) triple11) -> rule6)) -> rule5))] Gary is red.[(triple11)] Gary is round.[(triple12)] @1: Anne is cold.[(((triple1 triple4) -> rule6))] Erin is big.[(((triple7) -> rule2) OR ((triple6 triple7) -> rule3))] Gary is big.[(((triple12) -> rule2) OR ((triple9) -> rule4) OR ((triple10 triple12) -> rule3) OR ((((triple11 triple9) -> rule5) triple12) -> rule3))] @2: Erin is quiet.[(((((triple7) -> rule2)) -> rule1) OR ((((triple6 triple7) -> rule3)) -> rule1))] Gary is quiet.[(((((triple12) -> rule2)) -> rule1) OR ((((triple9) -> rule4)) -> rule1) OR ((((triple10 triple12) -> rule3)) -> rule1) OR ((((((triple11 triple9) -> rule5) triple12) -> rule3)) -> rule1))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is furry.
("Anne" "is" "furry" "+")
triple2
((triple4 ((triple1 triple4) -> (rule6 % int2))) -> (rule5 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
triple3
((triple1) -> (rule1 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
triple4
Anne is white.
("Anne" "is" "white" "+")
triple5
Erin is furry.
("Erin" "is" "furry" "+")
triple6
Erin is round.
("Erin" "is" "round" "+")
triple7
Erin is white.
("Erin" "is" "white" "+")
triple8
Gary is cold.
("Gary" "is" "cold" "+")
triple9
((((triple12) -> (rule2 % int2)) triple11) -> (rule6 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
((((triple10 triple12) -> (rule3 % int2)) triple11) -> (rule6 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
triple10
((triple11 triple9) -> (rule5 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
((triple11 ((((triple12) -> (rule2 % int3)) triple11) -> (rule6 % int2))) -> (rule5 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
int3
Gary is red.
("Gary" "is" "red" "+")
triple11
Gary is round.
("Gary" "is" "round" "+")
triple12
Anne is cold.
("Anne" "is" "cold" "+")
((triple1 triple4) -> (rule6 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
((triple7) -> (rule2 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
((triple6 triple7) -> (rule3 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
((triple12) -> (rule2 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
((triple9) -> (rule4 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
((triple10 triple12) -> (rule3 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
((((triple11 triple9) -> (rule5 % int2)) triple12) -> (rule3 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
((((triple7) -> (rule2 % int2))) -> (rule1 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
((((triple6 triple7) -> (rule3 % int2))) -> (rule1 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
((((triple12) -> (rule2 % int2))) -> (rule1 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
((((triple9) -> (rule4 % int2))) -> (rule1 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
((((triple10 triple12) -> (rule3 % int2))) -> (rule1 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
((((((triple11 triple9) -> (rule5 % int3)) triple12) -> (rule3 % int2))) -> (rule1 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
int3