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