Anne is green. Anne is red. Anne is rough. Anne is round. Bob is green. Bob is rough. Bob is round. Bob is not white. Dave is big. Dave is not red. Dave is rough. Dave is round. Dave is white. Harry is not big. Harry is not nice. If someone is big and not rough then they are not red. White people are not green.
Anne is green.
("Anne" "is" "green" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is round.
("Anne" "is" "round" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is not white.
("Bob" "is" "white" "-")
Dave is big.
("Dave" "is" "big" "+")
Dave is not red.
("Dave" "is" "red" "-")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is white.
("Dave" "is" "white" "+")
Harry is not big.
("Harry" "is" "big" "-")
Harry is not nice.
("Harry" "is" "nice" "-")
If someone is big and not rough then they are not red.
((("someone" "is" "big" "+") ("someone" "is" "rough" "~")) -> ("someone" "is" "red" "-"))
White people are not green.
((("someone" "is" "white" "+")) -> ("someone" "is" "green" "-"))
Bob is rough.
True
1
proof
[(triple6)]
("Bob" "is" "rough" "+")
triple6
Bob is not rough.
False
1
inv-proof
[(triple6)]
("Bob" "is" "rough" "-")
triple6
Dave is not green.
True
2
proof
[(((triple13) -> rule2))]
("Dave" "is" "green" "-")
((triple13) -> (rule2 % int1))
Dave is not green.
("Dave" "is" "green" "-")
int1
Dave is green.
False
2
inv-proof
[(((triple13) -> rule2))]
("Dave" "is" "green" "+")
((triple13) -> (rule2 % int1))
Dave is not green.
("Dave" "is" "green" "-")
int1
Bob is not red.
Unknown
inv-random
[@0: Bob is red.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "red" "-")
Bob is big.
Unknown
random
[@0: Bob is big.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "big" "+")
Harry is not red.
Unknown
inv-random
[@0: Harry is red.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "red" "-")
Anne is nice.
Unknown
random
[@0: Anne is nice.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "nice" "+")
@0: Anne is green.[(triple1)] Anne is red.[(triple2)] Anne is rough.[(triple3)] Anne is round.[(triple4)] Bob is green.[(triple5)] Bob is not white.[(triple8)] Bob is rough.[(triple6)] Bob is round.[(triple7)] Dave is big.[(triple9)] Dave is not red.[(triple10)] Dave is rough.[(triple11)] Dave is round.[(triple12)] Dave is white.[(triple13)] Harry is not big.[(triple14)] Harry is not nice.[(triple15)] @1: Dave is not green.[(((triple13) -> rule2))]
Anne is green.
("Anne" "is" "green" "+")
triple1
Anne is red.
("Anne" "is" "red" "+")
triple2
Anne is rough.
("Anne" "is" "rough" "+")
triple3
Anne is round.
("Anne" "is" "round" "+")
triple4
Bob is green.
("Bob" "is" "green" "+")
triple5
Bob is not white.
("Bob" "is" "white" "-")
triple8
Bob is rough.
("Bob" "is" "rough" "+")
triple6
Bob is round.
("Bob" "is" "round" "+")
triple7
Dave is big.
("Dave" "is" "big" "+")
triple9
Dave is not red.
("Dave" "is" "red" "-")
triple10
Dave is rough.
("Dave" "is" "rough" "+")
triple11
Dave is round.
("Dave" "is" "round" "+")
triple12
Dave is white.
("Dave" "is" "white" "+")
triple13
Harry is not big.
("Harry" "is" "big" "-")
triple14
Harry is not nice.
("Harry" "is" "nice" "-")
triple15
Dave is not green.
("Dave" "is" "green" "-")
((triple13) -> (rule2 % int1))
Dave is not green.
("Dave" "is" "green" "-")
int1