Anne is kind. Dave is kind. If someone is kind then they are quiet. If someone is round and nice then they are not quiet. If Anne is round then Anne is big. Green people are round. If Dave is quiet and Dave is kind then Dave is green. If Anne is round and Anne is not green then Anne is not smart.
Anne is kind.
("Anne" "is" "kind" "+")
Dave is kind.
("Dave" "is" "kind" "+")
If someone is kind then they are quiet.
((("someone" "is" "kind" "+")) -> ("someone" "is" "quiet" "+"))
If someone is round and nice then they are not quiet.
((("someone" "is" "round" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "quiet" "-"))
If Anne is round then Anne is big.
((("Anne" "is" "round" "+")) -> ("Anne" "is" "big" "+"))
Green people are round.
((("someone" "is" "green" "+")) -> ("someone" "is" "round" "+"))
If Dave is quiet and Dave is kind then Dave is green.
((("Dave" "is" "quiet" "+") ("Dave" "is" "kind" "+")) -> ("Dave" "is" "green" "+"))
If Anne is round and Anne is not green then Anne is not smart.
((("Anne" "is" "round" "+") ("Anne" "is" "green" "~")) -> ("Anne" "is" "smart" "-"))
Anne is kind.
True
1
proof
[(triple1)]
("Anne" "is" "kind" "+")
triple1
Anne is not kind.
False
1
inv-proof
[(triple1)]
("Anne" "is" "kind" "-")
triple1
Dave is quiet.
True
2
proof
[(((triple2) -> rule1))]
("Dave" "is" "quiet" "+")
((triple2) -> (rule1 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Anne is not quiet.
False
2
inv-proof
[(((triple1) -> rule1))]
("Anne" "is" "quiet" "-")
((triple1) -> (rule1 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Dave is green.
True
4
proof
[(((((triple2) -> rule1) triple2) -> rule5))]
("Dave" "is" "green" "+")
((((triple2) -> (rule1 % int2)) triple2) -> (rule5 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is not green.
False
4
inv-proof
[(((((triple2) -> rule1) triple2) -> rule5))]
("Dave" "is" "green" "-")
((((triple2) -> (rule1 % int2)) triple2) -> (rule5 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is round.
True
5
proof
[(((((((triple2) -> rule1) triple2) -> rule5)) -> rule4))]
("Dave" "is" "round" "+")
((((((triple2) -> (rule1 % int3)) triple2) -> (rule5 % int2))) -> (rule4 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
Dave is not round.
False
5
inv-proof
[(((((((triple2) -> rule1) triple2) -> rule5)) -> rule4))]
("Dave" "is" "round" "-")
((((((triple2) -> (rule1 % int3)) triple2) -> (rule5 % int2))) -> (rule4 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
Anne is not round.
Unknown
inv-rconc
[@1: Anne is round.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Anne" "is" "round" "-")
Anne is big.
Unknown
rconc
[@2: Anne is big.[CWA. Example of deepest failure = (rule3 <- rule4 <- FAIL)]]
("Anne" "is" "big" "+")
Anne is not nice.
Unknown
inv-random
[@0: Anne is nice.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "nice" "-")
Anne is smart.
Unknown
random
[@0: Anne is smart.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "smart" "+")
Dave is not smart.
Unknown
inv-random
[@0: Dave is smart.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "smart" "-")
Anne is green.
Unknown
random
[@0: Anne is green.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "green" "+")
Dave is not nice.
Unknown
inv-random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "-")
Dave is big.
Unknown
random
[@0: Dave is big.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "big" "+")
@0: Anne is kind.[(triple1)] Dave is kind.[(triple2)] @1: Anne is quiet.[(((triple1) -> rule1))] Dave is quiet.[(((triple2) -> rule1))] @2: Dave is green.[(((((triple2) -> rule1) triple2) -> rule5))] @3: Dave is round.[(((((((triple2) -> rule1) triple2) -> rule5)) -> rule4))]
Anne is kind.
("Anne" "is" "kind" "+")
triple1
Dave is kind.
("Dave" "is" "kind" "+")
triple2
Anne is quiet.
("Anne" "is" "quiet" "+")
((triple1) -> (rule1 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
((triple2) -> (rule1 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
((((triple2) -> (rule1 % int2)) triple2) -> (rule5 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
((((((triple2) -> (rule1 % int3)) triple2) -> (rule5 % int2))) -> (rule4 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3