Anne is red. Charlie is smart. Charlie is young. All quiet people are white. If Charlie is red and Charlie is quiet then Charlie is blue. Young people are smart. Young people are green. If someone is red then they are quiet. All quiet people are smart.
Anne is red.
("Anne" "is" "red" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Charlie is young.
("Charlie" "is" "young" "+")
All quiet people are white.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "white" "+"))
If Charlie is red and Charlie is quiet then Charlie is blue.
((("Charlie" "is" "red" "+") ("Charlie" "is" "quiet" "+")) -> ("Charlie" "is" "blue" "+"))
Young people are smart.
((("someone" "is" "young" "+")) -> ("someone" "is" "smart" "+"))
Young people are green.
((("someone" "is" "young" "+")) -> ("someone" "is" "green" "+"))
If someone is red then they are quiet.
((("someone" "is" "red" "+")) -> ("someone" "is" "quiet" "+"))
All quiet people are smart.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "smart" "+"))
Charlie is smart.
True
1
proof
[(triple2 OR ((triple3) -> rule3))]
("Charlie" "is" "smart" "+")
triple2
((triple3) -> (rule3 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Anne is not red.
False
1
inv-proof
[(triple1)]
("Anne" "is" "red" "-")
triple1
Charlie is green.
True
2
proof
[(((triple3) -> rule4))]
("Charlie" "is" "green" "+")
((triple3) -> (rule4 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Anne is not quiet.
False
2
inv-proof
[(((triple1) -> rule5))]
("Anne" "is" "quiet" "-")
((triple1) -> (rule5 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is smart.
True
3
proof
[(((((triple1) -> rule5)) -> rule6))]
("Anne" "is" "smart" "+")
((((triple1) -> (rule5 % int2))) -> (rule6 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is not white.
False
3
inv-proof
[(((((triple1) -> rule5)) -> rule1))]
("Anne" "is" "white" "-")
((((triple1) -> (rule5 % int2))) -> (rule1 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is not green.
Unknown
inv-rconc
[@1: Anne is green.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Anne" "is" "green" "-")
Charlie is white.
Unknown
rconc
[@2: Charlie is white.[CWA. Example of deepest failure = (rule1 <- rule5 <- FAIL)]]
("Charlie" "is" "white" "+")
Charlie is not quiet.
Unknown
inv-rconc
[@1: Charlie is quiet.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Charlie" "is" "quiet" "-")
Charlie is red.
Unknown
random
[@0: Charlie is red.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "red" "+")
Anne is not young.
Unknown
inv-random
[@0: Anne is young.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "young" "-")
Anne is blue.
Unknown
random
[@0: Anne is blue.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "blue" "+")
@0: Anne is red.[(triple1)] Charlie is smart.[(triple2 OR ((triple3) -> rule3))] Charlie is young.[(triple3)] @1: Anne is quiet.[(((triple1) -> rule5))] Charlie is green.[(((triple3) -> rule4))] @2: Anne is smart.[(((((triple1) -> rule5)) -> rule6))] Anne is white.[(((((triple1) -> rule5)) -> rule1))]
Anne is red.
("Anne" "is" "red" "+")
triple1
Charlie is smart.
("Charlie" "is" "smart" "+")
triple2
((triple3) -> (rule3 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
triple3
Anne is quiet.
("Anne" "is" "quiet" "+")
((triple1) -> (rule5 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
((triple3) -> (rule4 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
((((triple1) -> (rule5 % int2))) -> (rule6 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
((((triple1) -> (rule5 % int2))) -> (rule1 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2