Anne is blue. Charlie is quiet. Charlie is rough. All rough, green people are blue. If someone is quiet then they are white. If someone is white then they are green.
Anne is blue.
("Anne" "is" "blue" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
All rough, green people are blue.
((("someone" "is" "rough" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "blue" "+"))
If someone is quiet then they are white.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "white" "+"))
If someone is white then they are green.
((("someone" "is" "white" "+")) -> ("someone" "is" "green" "+"))
Anne is blue.
True
1
proof
[(triple1)]
("Anne" "is" "blue" "+")
triple1
Charlie is not rough.
False
1
inv-proof
[(triple3)]
("Charlie" "is" "rough" "-")
triple3
Charlie is white.
True
2
proof
[(((triple2) -> rule2))]
("Charlie" "is" "white" "+")
((triple2) -> (rule2 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is not white.
False
2
inv-proof
[(((triple2) -> rule2))]
("Charlie" "is" "white" "-")
((triple2) -> (rule2 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is green.
True
3
proof
[(((((triple2) -> rule2)) -> rule3))]
("Charlie" "is" "green" "+")
((((triple2) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is not green.
False
3
inv-proof
[(((((triple2) -> rule2)) -> rule3))]
("Charlie" "is" "green" "-")
((((triple2) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is blue.
True
5
proof
[(((triple3 ((((triple2) -> rule2)) -> rule3)) -> rule1))]
("Charlie" "is" "blue" "+")
((triple3 ((((triple2) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
Charlie is not blue.
False
5
inv-proof
[(((triple3 ((((triple2) -> rule2)) -> rule3)) -> rule1))]
("Charlie" "is" "blue" "-")
((triple3 ((((triple2) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
Anne is not white.
Unknown
inv-rconc
[@1: Anne is white.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Anne" "is" "white" "-")
Anne is green.
Unknown
rconc
[@2: Anne is green.[CWA. Example of deepest failure = (rule3 <- rule2 <- FAIL)]]
("Anne" "is" "green" "+")
Anne is not round.
Unknown
inv-random
[@0: Anne is round.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "round" "-")
Charlie is round.
Unknown
random
[@0: Charlie is round.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "round" "+")
Anne is not rough.
Unknown
inv-random
[@0: Anne is rough.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "rough" "-")
Charlie is kind.
Unknown
random
[@0: Charlie is kind.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "kind" "+")
Anne is not quiet.
Unknown
inv-random
[@0: Anne is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "quiet" "-")
Anne is kind.
Unknown
random
[@0: Anne is kind.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "kind" "+")
@0: Anne is blue.[(triple1)] Charlie is quiet.[(triple2)] Charlie is rough.[(triple3)] @1: Charlie is white.[(((triple2) -> rule2))] @2: Charlie is green.[(((((triple2) -> rule2)) -> rule3))] @3: Charlie is blue.[(((triple3 ((((triple2) -> rule2)) -> rule3)) -> rule1))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple2
Charlie is rough.
("Charlie" "is" "rough" "+")
triple3
Charlie is white.
("Charlie" "is" "white" "+")
((triple2) -> (rule2 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
((((triple2) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
((triple3 ((((triple2) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3