Anne is not green. Charlie is big. If something is big then it is quiet. If something is furry then it is big. If Charlie is quiet and Charlie is big then Charlie is young. Kind things are cold. If Anne is kind then Anne is not green. If something is big and not quiet then it is kind.
Anne is not green.
("Anne" "is" "green" "-")
Charlie is big.
("Charlie" "is" "big" "+")
If something is big then it is quiet.
((("something" "is" "big" "+")) -> ("something" "is" "quiet" "+"))
If something is furry then it is big.
((("something" "is" "furry" "+")) -> ("something" "is" "big" "+"))
If Charlie is quiet and Charlie is big then Charlie is young.
((("Charlie" "is" "quiet" "+") ("Charlie" "is" "big" "+")) -> ("Charlie" "is" "young" "+"))
Kind things are cold.
((("something" "is" "kind" "+")) -> ("something" "is" "cold" "+"))
If Anne is kind then Anne is not green.
((("Anne" "is" "kind" "+")) -> ("Anne" "is" "green" "-"))
If something is big and not quiet then it is kind.
((("something" "is" "big" "+") ("something" "is" "quiet" "~")) -> ("something" "is" "kind" "+"))
Charlie is big.
True
1
proof
[(triple2)]
("Charlie" "is" "big" "+")
triple2
Charlie is not big.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "big" "-")
triple2
Charlie is quiet.
True
2
proof
[(((triple2) -> rule1))]
("Charlie" "is" "quiet" "+")
((triple2) -> (rule1 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is not quiet.
False
2
inv-proof
[(((triple2) -> rule1))]
("Charlie" "is" "quiet" "-")
((triple2) -> (rule1 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is young.
True
4
proof
[(((((triple2) -> rule1) triple2) -> rule3))]
("Charlie" "is" "young" "+")
((((triple2) -> (rule1 % int2)) triple2) -> (rule3 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is not young.
False
4
inv-proof
[(((((triple2) -> rule1) triple2) -> rule3))]
("Charlie" "is" "young" "-")
((((triple2) -> (rule1 % int2)) triple2) -> (rule3 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is not cold.
Unknown
inv-rconc
[@2: Charlie is cold.[CWA. Example of deepest failure = (rule4 <- rule6 <- FAIL)]]
("Charlie" "is" "cold" "-")
Charlie is kind.
Unknown
rconc
[@1: Charlie is kind.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Charlie" "is" "kind" "+")
Anne is not kind.
Unknown
inv-rconc
[@1: Anne is kind.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Anne" "is" "kind" "-")
Charlie is green.
Unknown
random
[@0: Charlie is green.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "green" "+")
Anne is not furry.
Unknown
inv-random
[@0: Anne is furry.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "furry" "-")
Charlie is furry.
Unknown
random
[@0: Charlie is furry.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "furry" "+")
@0: Anne is not green.[(triple1)] Charlie is big.[(triple2)] @1: Charlie is quiet.[(((triple2) -> rule1))] @2: Charlie is young.[(((((triple2) -> rule1) triple2) -> rule3))]
Anne is not green.
("Anne" "is" "green" "-")
triple1
Charlie is big.
("Charlie" "is" "big" "+")
triple2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((triple2) -> (rule1 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
((((triple2) -> (rule1 % int2)) triple2) -> (rule3 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2