Dave is big. Dave is furry. Dave is smart. Dave is white. Dave is young. Gary is big. Gary is cold. Gary is furry. Gary is green. Gary is white. If Dave is smart then Dave is white.
Dave is big.
("Dave" "is" "big" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is smart.
("Dave" "is" "smart" "+")
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 furry.
("Gary" "is" "furry" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is white.
("Gary" "is" "white" "+")
If Dave is smart then Dave is white.
((("Dave" "is" "smart" "+")) -> ("Dave" "is" "white" "+"))
Dave is furry.
True
1
proof
[(triple2)]
("Dave" "is" "furry" "+")
triple2
Dave is not big.
False
1
inv-proof
[(triple1)]
("Dave" "is" "big" "-")
triple1
Dave is not green.
Unknown
inv-random
[@0: Dave is green.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "green" "-")
Gary is young.
Unknown
random
[@0: Gary is young.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "young" "+")
@0: Dave is big.[(triple1)] Dave is furry.[(triple2)] Dave is smart.[(triple3)] Dave is white.[(triple4 OR ((triple3) -> rule1))] Dave is young.[(triple5)] Gary is big.[(triple6)] Gary is cold.[(triple7)] Gary is furry.[(triple8)] Gary is green.[(triple9)] Gary is white.[(triple10)]
Dave is big.
("Dave" "is" "big" "+")
triple1
Dave is furry.
("Dave" "is" "furry" "+")
triple2
Dave is smart.
("Dave" "is" "smart" "+")
triple3
Dave is white.
("Dave" "is" "white" "+")
triple4
((triple3) -> (rule1 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
triple5
Gary is big.
("Gary" "is" "big" "+")
triple6
Gary is cold.
("Gary" "is" "cold" "+")
triple7
Gary is furry.
("Gary" "is" "furry" "+")
triple8
Gary is green.
("Gary" "is" "green" "+")
triple9
Gary is white.
("Gary" "is" "white" "+")
triple10