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