Anne is round. Charlie is red. Gary is not rough. All quiet, red people are smart. If someone is quiet then they are smart. All cold people are smart. All quiet people are blue. If Charlie is smart then Charlie is not blue. If someone is blue then they are rough. If Anne is cold then Anne is rough. All red people are cold.
Anne is round.
("Anne" "is" "round" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Gary is not rough.
("Gary" "is" "rough" "-")
All quiet, red people are smart.
((("someone" "is" "quiet" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "smart" "+"))
If someone is quiet then they are smart.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "smart" "+"))
All cold people are smart.
((("someone" "is" "cold" "+")) -> ("someone" "is" "smart" "+"))
All quiet people are blue.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "blue" "+"))
If Charlie is smart then Charlie is not blue.
((("Charlie" "is" "smart" "+")) -> ("Charlie" "is" "blue" "-"))
If someone is blue then they are rough.
((("someone" "is" "blue" "+")) -> ("someone" "is" "rough" "+"))
If Anne is cold then Anne is rough.
((("Anne" "is" "cold" "+")) -> ("Anne" "is" "rough" "+"))
All red people are cold.
((("someone" "is" "red" "+")) -> ("someone" "is" "cold" "+"))
Gary is not rough.
True
1
proof
[(triple3)]
("Gary" "is" "rough" "-")
triple3
Anne is not round.
False
1
inv-proof
[(triple1)]
("Anne" "is" "round" "-")
triple1
Charlie is cold.
True
2
proof
[(((triple2) -> rule8))]
("Charlie" "is" "cold" "+")
((triple2) -> (rule8 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is not cold.
False
2
inv-proof
[(((triple2) -> rule8))]
("Charlie" "is" "cold" "-")
((triple2) -> (rule8 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is smart.
True
3
proof
[(((((triple2) -> rule8)) -> rule3))]
("Charlie" "is" "smart" "+")
((((triple2) -> (rule8 % int2))) -> (rule3 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is not smart.
False
3
inv-proof
[(((((triple2) -> rule8)) -> rule3))]
("Charlie" "is" "smart" "-")
((((triple2) -> (rule8 % int2))) -> (rule3 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is not blue.
True
4
proof
[(((((((triple2) -> rule8)) -> rule3)) -> rule5))]
("Charlie" "is" "blue" "-")
((((((triple2) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Charlie is not blue.
("Charlie" "is" "blue" "-")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3
Charlie is blue.
False
4
inv-proof
[(((((((triple2) -> rule8)) -> rule3)) -> rule5))]
("Charlie" "is" "blue" "+")
((((((triple2) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Charlie is not blue.
("Charlie" "is" "blue" "-")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3
Gary is not blue.
Unknown
inv-rconc
[@1: Gary is blue.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Gary" "is" "blue" "-")
Charlie is rough.
Unknown
rconc
[@1: Charlie is rough.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Charlie" "is" "rough" "+")
Gary is not cold.
Unknown
inv-rconc
[@1: Gary is cold.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Gary" "is" "cold" "-")
Anne is rough.
Unknown
rconc
[@2: Anne is rough.[CWA. Example of deepest failure = (rule6 <- rule4 <- FAIL)]]
("Anne" "is" "rough" "+")
Gary is not red.
Unknown
inv-random
[@0: Gary is red.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "red" "-")
Gary is round.
Unknown
random
[@0: Gary is round.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "round" "+")
Anne is not red.
Unknown
inv-random
[@0: Anne is red.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "red" "-")
Gary is quiet.
Unknown
random
[@0: Gary is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "quiet" "+")
@0: Anne is round.[(triple1)] Charlie is red.[(triple2)] Gary is not rough.[(triple3)] @1: Charlie is cold.[(((triple2) -> rule8))] @2: Charlie is smart.[(((((triple2) -> rule8)) -> rule3))] @3: Charlie is not blue.[(((((((triple2) -> rule8)) -> rule3)) -> rule5))]
Anne is round.
("Anne" "is" "round" "+")
triple1
Charlie is red.
("Charlie" "is" "red" "+")
triple2
Gary is not rough.
("Gary" "is" "rough" "-")
triple3
Charlie is cold.
("Charlie" "is" "cold" "+")
((triple2) -> (rule8 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
((((triple2) -> (rule8 % int2))) -> (rule3 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is not blue.
("Charlie" "is" "blue" "-")
((((((triple2) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Charlie is not blue.
("Charlie" "is" "blue" "-")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3