Dave is big. Dave is blue. Dave is furry. Dave is green. Dave is kind. Dave is red. Gary is blue. Gary is furry. Gary is green. Gary is kind. Gary is red. Gary is round. Blue things are red.
Dave is big.
("Dave" "is" "big" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is red.
("Dave" "is" "red" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is round.
("Gary" "is" "round" "+")
Blue things are red.
((("something" "is" "blue" "+")) -> ("something" "is" "red" "+"))
Gary is round.
True
1
proof
[(triple12)]
("Gary" "is" "round" "+")
triple12
Gary is not red.
False
1
inv-proof
[(triple11 OR ((triple7) -> rule1))]
("Gary" "is" "red" "-")
triple11
((triple7) -> (rule1 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Dave is not round.
Unknown
inv-random
[@0: Dave is round.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "round" "-")
Gary is big.
Unknown
random
[@0: Gary is big.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "big" "+")
@0: Dave is big.[(triple1)] Dave is blue.[(triple2)] Dave is furry.[(triple3)] Dave is green.[(triple4)] Dave is kind.[(triple5)] Dave is red.[(triple6 OR ((triple2) -> rule1))] Gary is blue.[(triple7)] Gary is furry.[(triple8)] Gary is green.[(triple9)] Gary is kind.[(triple10)] Gary is red.[(triple11 OR ((triple7) -> rule1))] Gary is round.[(triple12)]
Dave is big.
("Dave" "is" "big" "+")
triple1
Dave is blue.
("Dave" "is" "blue" "+")
triple2
Dave is furry.
("Dave" "is" "furry" "+")
triple3
Dave is green.
("Dave" "is" "green" "+")
triple4
Dave is kind.
("Dave" "is" "kind" "+")
triple5
Dave is red.
("Dave" "is" "red" "+")
triple6
((triple2) -> (rule1 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
triple7
Gary is furry.
("Gary" "is" "furry" "+")
triple8
Gary is green.
("Gary" "is" "green" "+")
triple9
Gary is kind.
("Gary" "is" "kind" "+")
triple10
Gary is red.
("Gary" "is" "red" "+")
triple11
((triple7) -> (rule1 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
triple12