Anne is blue. Anne is green. Anne is quiet. Anne is not rough. Anne is round. Charlie is cold. Charlie is not rough. Charlie is round. Charlie is white. Gary is cold. Gary is not quiet. Gary is rough. If someone is blue then they are cold. Blue people are cold. If Gary is blue and Gary is cold then Gary is not rough. Round, cold people are white. If someone is green and round then they are blue. If Anne is blue and Anne is not cold then Anne is not white.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is not rough.
("Anne" "is" "rough" "-")
Anne is round.
("Anne" "is" "round" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is not rough.
("Charlie" "is" "rough" "-")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is not quiet.
("Gary" "is" "quiet" "-")
Gary is rough.
("Gary" "is" "rough" "+")
If someone is blue then they are cold.
((("someone" "is" "blue" "+")) -> ("someone" "is" "cold" "+"))
Blue people are cold.
((("someone" "is" "blue" "+")) -> ("someone" "is" "cold" "+"))
If Gary is blue and Gary is cold then Gary is not rough.
((("Gary" "is" "blue" "+") ("Gary" "is" "cold" "+")) -> ("Gary" "is" "rough" "-"))
Round, cold people are white.
((("someone" "is" "round" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "white" "+"))
If someone is green and round then they are blue.
((("someone" "is" "green" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "blue" "+"))
If Anne is blue and Anne is not cold then Anne is not white.
((("Anne" "is" "blue" "+") ("Anne" "is" "cold" "~")) -> ("Anne" "is" "white" "-"))
Charlie is round.
True
1
proof
[(triple8)]
("Charlie" "is" "round" "+")
triple8
Anne is not green.
False
1
inv-proof
[(triple2)]
("Anne" "is" "green" "-")
triple2
Anne is cold.
True
2
proof
[(((triple1) -> rule1) OR ((triple1) -> rule2) OR ((((triple2 triple5) -> rule5)) -> rule1) OR ((((triple2 triple5) -> rule5)) -> rule2))]
("Anne" "is" "cold" "+")
((triple1) -> (rule1 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
((triple1) -> (rule2 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
((((triple2 triple5) -> (rule5 % int2))) -> (rule1 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
((((triple2 triple5) -> (rule5 % int2))) -> (rule2 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is not cold.
False
2
inv-proof
[(((triple1) -> rule1) OR ((triple1) -> rule2) OR ((((triple2 triple5) -> rule5)) -> rule1) OR ((((triple2 triple5) -> rule5)) -> rule2))]
("Anne" "is" "cold" "-")
((triple1) -> (rule1 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
((triple1) -> (rule2 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
((((triple2 triple5) -> (rule5 % int2))) -> (rule1 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
((((triple2 triple5) -> (rule5 % int2))) -> (rule2 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is white.
True
4
proof
[(((triple5 ((triple1) -> rule1)) -> rule4) OR ((triple5 ((triple1) -> rule2)) -> rule4) OR ((triple5 ((((triple2 triple5) -> rule5)) -> rule1)) -> rule4) OR ((triple5 ((((triple2 triple5) -> rule5)) -> rule2)) -> rule4))]
("Anne" "is" "white" "+")
((triple5 ((triple1) -> (rule1 % int2))) -> (rule4 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
((triple5 ((triple1) -> (rule2 % int2))) -> (rule4 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
((triple5 ((((triple2 triple5) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3
((triple5 ((((triple2 triple5) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3
Anne is not white.
False
4
inv-proof
[(((triple5 ((triple1) -> rule1)) -> rule4) OR ((triple5 ((triple1) -> rule2)) -> rule4) OR ((triple5 ((((triple2 triple5) -> rule5)) -> rule1)) -> rule4) OR ((triple5 ((((triple2 triple5) -> rule5)) -> rule2)) -> rule4))]
("Anne" "is" "white" "-")
((triple5 ((triple1) -> (rule1 % int2))) -> (rule4 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
((triple5 ((triple1) -> (rule2 % int2))) -> (rule4 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
((triple5 ((((triple2 triple5) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3
((triple5 ((((triple2 triple5) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3
Gary is not blue.
Unknown
inv-rconc
[@1: Gary is blue.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Gary" "is" "blue" "-")
Gary is white.
Unknown
rconc
[@1: Gary is white.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Gary" "is" "white" "+")
Charlie is not blue.
Unknown
inv-rconc
[@1: Charlie is blue.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Charlie" "is" "blue" "-")
Charlie is quiet.
Unknown
random
[@0: Charlie is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "quiet" "+")
Gary is not round.
Unknown
inv-random
[@0: Gary is round.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "round" "-")
Charlie is green.
Unknown
random
[@0: Charlie is green.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "green" "+")
@0: Anne is blue.[(triple1 OR ((triple2 triple5) -> rule5))] Anne is green.[(triple2)] Anne is not rough.[(triple4)] Anne is quiet.[(triple3)] Anne is round.[(triple5)] Charlie is cold.[(triple6)] Charlie is not rough.[(triple7)] Charlie is round.[(triple8)] Charlie is white.[(triple9 OR ((triple8 triple6) -> rule4))] Gary is cold.[(triple10)] Gary is not quiet.[(triple11)] Gary is rough.[(triple12)] @1: Anne is cold.[(((triple1) -> rule1) OR ((triple1) -> rule2) OR ((((triple2 triple5) -> rule5)) -> rule1) OR ((((triple2 triple5) -> rule5)) -> rule2))] @2: Anne is white.[(((triple5 ((triple1) -> rule1)) -> rule4) OR ((triple5 ((triple1) -> rule2)) -> rule4) OR ((triple5 ((((triple2 triple5) -> rule5)) -> rule1)) -> rule4) OR ((triple5 ((((triple2 triple5) -> rule5)) -> rule2)) -> rule4))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
((triple2 triple5) -> (rule5 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
triple2
Anne is not rough.
("Anne" "is" "rough" "-")
triple4
Anne is quiet.
("Anne" "is" "quiet" "+")
triple3
Anne is round.
("Anne" "is" "round" "+")
triple5
Charlie is cold.
("Charlie" "is" "cold" "+")
triple6
Charlie is not rough.
("Charlie" "is" "rough" "-")
triple7
Charlie is round.
("Charlie" "is" "round" "+")
triple8
Charlie is white.
("Charlie" "is" "white" "+")
triple9
((triple8 triple6) -> (rule4 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
triple10
Gary is not quiet.
("Gary" "is" "quiet" "-")
triple11
Gary is rough.
("Gary" "is" "rough" "+")
triple12
Anne is cold.
("Anne" "is" "cold" "+")
((triple1) -> (rule1 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
((triple1) -> (rule2 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
((((triple2 triple5) -> (rule5 % int2))) -> (rule1 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
((((triple2 triple5) -> (rule5 % int2))) -> (rule2 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
((triple5 ((triple1) -> (rule1 % int2))) -> (rule4 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
((triple5 ((triple1) -> (rule2 % int2))) -> (rule4 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
((triple5 ((((triple2 triple5) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3
((triple5 ((((triple2 triple5) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3