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