Anne is big. Anne is cold. Anne is rough. Anne is round. Anne is not smart. Anne is white. Anne is young. Bob is rough. Bob is round. Dave is big. Dave is white. Dave is young. Gary is big. Gary is cold. Gary is smart. Gary is young. If Gary is big and Gary is cold then Gary is not round.
Anne is big.
("Anne" "is" "big" "+")
Anne is cold.
("Anne" "is" "cold" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is round.
("Anne" "is" "round" "+")
Anne is not smart.
("Anne" "is" "smart" "-")
Anne is white.
("Anne" "is" "white" "+")
Anne is young.
("Anne" "is" "young" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is round.
("Bob" "is" "round" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is white.
("Dave" "is" "white" "+")
Dave is young.
("Dave" "is" "young" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Gary is young.
("Gary" "is" "young" "+")
If Gary is big and Gary is cold then Gary is not round.
((("Gary" "is" "big" "+") ("Gary" "is" "cold" "+")) -> ("Gary" "is" "round" "-"))
Dave is big.
True
1
proof
[(triple10)]
("Dave" "is" "big" "+")
triple10
Gary is not big.
False
1
inv-proof
[(triple13)]
("Gary" "is" "big" "-")
triple13
Gary is not round.
True
3
proof
[(((triple13 triple14) -> rule1))]
("Gary" "is" "round" "-")
((triple13 triple14) -> (rule1 % int1))
Gary is not round.
("Gary" "is" "round" "-")
int1
Gary is round.
False
3
inv-proof
[(((triple13 triple14) -> rule1))]
("Gary" "is" "round" "+")
((triple13 triple14) -> (rule1 % int1))
Gary is not round.
("Gary" "is" "round" "-")
int1
Bob is not smart.
Unknown
inv-random
[@0: Bob is smart.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "smart" "-")
Dave is cold.
Unknown
random
[@0: Dave is cold.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "cold" "+")
Gary is not rough.
Unknown
inv-random
[@0: Gary is rough.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "rough" "-")
Bob is young.
Unknown
random
[@0: Bob is young.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "young" "+")
@0: Anne is big.[(triple1)] Anne is cold.[(triple2)] Anne is not smart.[(triple5)] Anne is rough.[(triple3)] Anne is round.[(triple4)] Anne is white.[(triple6)] Anne is young.[(triple7)] Bob is rough.[(triple8)] Bob is round.[(triple9)] Dave is big.[(triple10)] Dave is white.[(triple11)] Dave is young.[(triple12)] Gary is big.[(triple13)] Gary is cold.[(triple14)] Gary is smart.[(triple15)] Gary is young.[(triple16)] @1: Gary is not round.[(((triple13 triple14) -> rule1))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is cold.
("Anne" "is" "cold" "+")
triple2
Anne is not smart.
("Anne" "is" "smart" "-")
triple5
Anne is rough.
("Anne" "is" "rough" "+")
triple3
Anne is round.
("Anne" "is" "round" "+")
triple4
Anne is white.
("Anne" "is" "white" "+")
triple6
Anne is young.
("Anne" "is" "young" "+")
triple7
Bob is rough.
("Bob" "is" "rough" "+")
triple8
Bob is round.
("Bob" "is" "round" "+")
triple9
Dave is big.
("Dave" "is" "big" "+")
triple10
Dave is white.
("Dave" "is" "white" "+")
triple11
Dave is young.
("Dave" "is" "young" "+")
triple12
Gary is big.
("Gary" "is" "big" "+")
triple13
Gary is cold.
("Gary" "is" "cold" "+")
triple14
Gary is smart.
("Gary" "is" "smart" "+")
triple15
Gary is young.
("Gary" "is" "young" "+")
triple16
Gary is not round.
("Gary" "is" "round" "-")
((triple13 triple14) -> (rule1 % int1))
Gary is not round.
("Gary" "is" "round" "-")
int1