Anne is red. Harry is red. Kind people are smart. Quiet people are smart. If someone is red then they are not kind. If Harry is red then Harry is quiet. All white people are not round. If someone is smart and not quiet then they are not round.
Anne is red.
("Anne" "is" "red" "+")
Harry is red.
("Harry" "is" "red" "+")
Kind people are smart.
((("someone" "is" "kind" "+")) -> ("someone" "is" "smart" "+"))
Quiet people are smart.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "smart" "+"))
If someone is red then they are not kind.
((("someone" "is" "red" "+")) -> ("someone" "is" "kind" "-"))
If Harry is red then Harry is quiet.
((("Harry" "is" "red" "+")) -> ("Harry" "is" "quiet" "+"))
All white people are not round.
((("someone" "is" "white" "+")) -> ("someone" "is" "round" "-"))
If someone is smart and not quiet then they are not round.
((("someone" "is" "smart" "+") ("someone" "is" "quiet" "~")) -> ("someone" "is" "round" "-"))
Anne is red.
True
1
proof
[(triple1)]
("Anne" "is" "red" "+")
triple1
Harry is not red.
False
1
inv-proof
[(triple2)]
("Harry" "is" "red" "-")
triple2
Harry is not kind.
True
2
proof
[(((triple2) -> rule3))]
("Harry" "is" "kind" "-")
((triple2) -> (rule3 % int1))
Harry is not kind.
("Harry" "is" "kind" "-")
int1
Harry is kind.
False
2
inv-proof
[(((triple2) -> rule3))]
("Harry" "is" "kind" "+")
((triple2) -> (rule3 % int1))
Harry is not kind.
("Harry" "is" "kind" "-")
int1
Harry is smart.
True
3
proof
[(((((triple2) -> rule4)) -> rule2))]
("Harry" "is" "smart" "+")
((((triple2) -> (rule4 % int2))) -> (rule2 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is not smart.
False
3
inv-proof
[(((((triple2) -> rule4)) -> rule2))]
("Harry" "is" "smart" "-")
((((triple2) -> (rule4 % int2))) -> (rule2 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Anne is not smart.
Unknown
inv-rconc
[@1: Anne is smart.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Anne" "is" "smart" "-")
Anne is white.
Unknown
random
[@0: Anne is white.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "white" "+")
Anne is not quiet.
Unknown
inv-random
[@0: Anne is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "quiet" "-")
Harry is round.
Unknown
random
[@0: Harry is round.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "round" "+")
Harry is not big.
Unknown
inv-random
[@0: Harry is big.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "big" "-")
Anne is big.
Unknown
random
[@0: Anne is big.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "big" "+")
@0: Anne is red.[(triple1)] Harry is red.[(triple2)] @1: Anne is not kind.[(((triple1) -> rule3))] Harry is not kind.[(((triple2) -> rule3))] Harry is quiet.[(((triple2) -> rule4))] @2: Harry is smart.[(((((triple2) -> rule4)) -> rule2))]
Anne is red.
("Anne" "is" "red" "+")
triple1
Harry is red.
("Harry" "is" "red" "+")
triple2
Anne is not kind.
("Anne" "is" "kind" "-")
((triple1) -> (rule3 % int1))
Anne is not kind.
("Anne" "is" "kind" "-")
int1
Harry is not kind.
("Harry" "is" "kind" "-")
((triple2) -> (rule3 % int1))
Harry is not kind.
("Harry" "is" "kind" "-")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
((triple2) -> (rule4 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
((((triple2) -> (rule4 % int2))) -> (rule2 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2