Anne is big. Anne is round. Charlie is quiet. If Charlie is not round then Charlie is blue. All round, big people are blue. If someone is blue and big then they are not nice. If Anne is nice then Anne is blue. If Charlie is nice then Charlie is big. If someone is big and not nice then they are quiet.
Anne is big.
("Anne" "is" "big" "+")
Anne is round.
("Anne" "is" "round" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
If Charlie is not round then Charlie is blue.
((("Charlie" "is" "round" "~")) -> ("Charlie" "is" "blue" "+"))
All round, big people are blue.
((("someone" "is" "round" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "blue" "+"))
If someone is blue and big then they are not nice.
((("someone" "is" "blue" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "nice" "-"))
If Anne is nice then Anne is blue.
((("Anne" "is" "nice" "+")) -> ("Anne" "is" "blue" "+"))
If Charlie is nice then Charlie is big.
((("Charlie" "is" "nice" "+")) -> ("Charlie" "is" "big" "+"))
If someone is big and not nice then they are quiet.
((("someone" "is" "big" "+") ("someone" "is" "nice" "~")) -> ("someone" "is" "quiet" "+"))
Anne is big.
True
1
proof
[(triple1)]
("Anne" "is" "big" "+")
triple1
Charlie is not quiet.
False
1
inv-proof
[(triple3)]
("Charlie" "is" "quiet" "-")
triple3
Anne is blue.
True
3
proof
[(((triple2 triple1) -> rule2))]
("Anne" "is" "blue" "+")
((triple2 triple1) -> (rule2 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is not blue.
False
3
inv-proof
[(((triple2 triple1) -> rule2))]
("Anne" "is" "blue" "-")
((triple2 triple1) -> (rule2 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is not nice.
True
5
proof
[(((((triple2 triple1) -> rule2) triple1) -> rule3))]
("Anne" "is" "nice" "-")
((((triple2 triple1) -> (rule2 % int2)) triple1) -> (rule3 % int1))
Anne is not nice.
("Anne" "is" "nice" "-")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is nice.
False
5
inv-proof
[(((((triple2 triple1) -> rule2) triple1) -> rule3))]
("Anne" "is" "nice" "+")
((((triple2 triple1) -> (rule2 % int2)) triple1) -> (rule3 % int1))
Anne is not nice.
("Anne" "is" "nice" "-")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is quiet.
True
7
proof
[(((triple1 ((((triple2 triple1) -> rule2) triple1) -> rule3)) -> rule6))]
("Anne" "is" "quiet" "+")
((triple1 ((((triple2 triple1) -> (rule2 % int3)) triple1) -> (rule3 % int2))) -> (rule6 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is not nice.
("Anne" "is" "nice" "-")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3
Anne is not quiet.
False
7
inv-proof
[(((triple1 ((((triple2 triple1) -> rule2) triple1) -> rule3)) -> rule6))]
("Anne" "is" "quiet" "-")
((triple1 ((((triple2 triple1) -> (rule2 % int3)) triple1) -> (rule3 % int2))) -> (rule6 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is not nice.
("Anne" "is" "nice" "-")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3
Charlie is not big.
Unknown
inv-rconc
[@1: Charlie is big.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Charlie" "is" "big" "-")
Charlie is blue.
Unknown
rconc
[@1: Charlie is blue.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "blue" "+")
Charlie is not nice.
Unknown
inv-random
[@0: Charlie is nice.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "nice" "-")
Charlie is round.
Unknown
random
[@0: Charlie is round.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "round" "+")
Anne is not white.
Unknown
inv-random
[@0: Anne is white.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "white" "-")
Anne is smart.
Unknown
random
[@0: Anne is smart.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "smart" "+")
Charlie is not white.
Unknown
inv-random
[@0: Charlie is white.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "white" "-")
Charlie is smart.
Unknown
random
[@0: Charlie is smart.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "smart" "+")
@0: Anne is big.[(triple1)] Anne is round.[(triple2)] Charlie is quiet.[(triple3)] @1: Anne is blue.[(((triple2 triple1) -> rule2))] @2: Anne is not nice.[(((((triple2 triple1) -> rule2) triple1) -> rule3))] @3: Anne is quiet.[(((triple1 ((((triple2 triple1) -> rule2) triple1) -> rule3)) -> rule6))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is round.
("Anne" "is" "round" "+")
triple2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple3
Anne is blue.
("Anne" "is" "blue" "+")
((triple2 triple1) -> (rule2 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is not nice.
("Anne" "is" "nice" "-")
((((triple2 triple1) -> (rule2 % int2)) triple1) -> (rule3 % int1))
Anne is not nice.
("Anne" "is" "nice" "-")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
((triple1 ((((triple2 triple1) -> (rule2 % int3)) triple1) -> (rule3 % int2))) -> (rule6 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is not nice.
("Anne" "is" "nice" "-")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3