Anne is blue. Anne is quiet. Charlie is white. All kind, smart things are green. If something is white then it is kind. If something is green and white then it is round. All quiet things are blue. If something is white and kind then it is round. If Charlie is white and Charlie is quiet then Charlie is blue. All smart things are round. Round things are green.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Charlie is white.
("Charlie" "is" "white" "+")
All kind, smart things are green.
((("something" "is" "kind" "+") ("something" "is" "smart" "+")) -> ("something" "is" "green" "+"))
If something is white then it is kind.
((("something" "is" "white" "+")) -> ("something" "is" "kind" "+"))
If something is green and white then it is round.
((("something" "is" "green" "+") ("something" "is" "white" "+")) -> ("something" "is" "round" "+"))
All quiet things are blue.
((("something" "is" "quiet" "+")) -> ("something" "is" "blue" "+"))
If something is white and kind then it is round.
((("something" "is" "white" "+") ("something" "is" "kind" "+")) -> ("something" "is" "round" "+"))
If Charlie is white and Charlie is quiet then Charlie is blue.
((("Charlie" "is" "white" "+") ("Charlie" "is" "quiet" "+")) -> ("Charlie" "is" "blue" "+"))
All smart things are round.
((("something" "is" "smart" "+")) -> ("something" "is" "round" "+"))
Round things are green.
((("something" "is" "round" "+")) -> ("something" "is" "green" "+"))
Charlie is white.
True
1
proof
[(triple3)]
("Charlie" "is" "white" "+")
triple3
Anne is not quiet.
False
1
inv-proof
[(triple2)]
("Anne" "is" "quiet" "-")
triple2
Charlie is kind.
True
2
proof
[(((triple3) -> rule2))]
("Charlie" "is" "kind" "+")
((triple3) -> (rule2 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is not kind.
False
2
inv-proof
[(((triple3) -> rule2))]
("Charlie" "is" "kind" "-")
((triple3) -> (rule2 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is round.
True
4
proof
[(((triple3 ((triple3) -> rule2)) -> rule5))]
("Charlie" "is" "round" "+")
((triple3 ((triple3) -> (rule2 % int2))) -> (rule5 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is not round.
False
4
inv-proof
[(((triple3 ((triple3) -> rule2)) -> rule5))]
("Charlie" "is" "round" "-")
((triple3 ((triple3) -> (rule2 % int2))) -> (rule5 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is green.
True
5
proof
[(((((triple3 ((triple3) -> rule2)) -> rule5)) -> rule8))]
("Charlie" "is" "green" "+")
((((triple3 ((triple3) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
Charlie is not green.
False
5
inv-proof
[(((((triple3 ((triple3) -> rule2)) -> rule5)) -> rule8))]
("Charlie" "is" "green" "-")
((((triple3 ((triple3) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
Anne is not round.
Unknown
inv-rconc
[@1: Anne is round.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Anne" "is" "round" "-")
Anne is kind.
Unknown
rconc
[@1: Anne is kind.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Anne" "is" "kind" "+")
Charlie is not blue.
Unknown
inv-rconc
[@1: Charlie is blue.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Charlie" "is" "blue" "-")
Anne is green.
Unknown
rconc
[@2: Anne is green.[CWA. Example of deepest failure = (rule8 <- rule3 <- FAIL)]]
("Anne" "is" "green" "+")
Anne is not smart.
Unknown
inv-random
[@0: Anne is smart.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "smart" "-")
Charlie is quiet.
Unknown
random
[@0: Charlie is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "quiet" "+")
Charlie is not smart.
Unknown
inv-random
[@0: Charlie is smart.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "smart" "-")
Anne is white.
Unknown
random
[@0: Anne is white.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "white" "+")
@0: Anne is blue.[(triple1 OR ((triple2) -> rule4))] Anne is quiet.[(triple2)] Charlie is white.[(triple3)] @1: Charlie is kind.[(((triple3) -> rule2))] @2: Charlie is round.[(((triple3 ((triple3) -> rule2)) -> rule5))] @3: Charlie is green.[(((((triple3 ((triple3) -> rule2)) -> rule5)) -> rule8))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
((triple2) -> (rule4 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
triple2
Charlie is white.
("Charlie" "is" "white" "+")
triple3
Charlie is kind.
("Charlie" "is" "kind" "+")
((triple3) -> (rule2 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
((triple3 ((triple3) -> (rule2 % int2))) -> (rule5 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
((((triple3 ((triple3) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3