Dave is big. Dave is blue. Dave is furry. Dave is smart. Dave is white. Gary is green. Gary is smart. White people are blue. Green, blue people are big. All smart people are blue. White, smart people are big. All green people are furry. All big, green people are blue.
Dave is big.
("Dave" "is" "big" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is white.
("Dave" "is" "white" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is smart.
("Gary" "is" "smart" "+")
White people are blue.
((("someone" "is" "white" "+")) -> ("someone" "is" "blue" "+"))
Green, blue people are big.
((("someone" "is" "green" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "big" "+"))
All smart people are blue.
((("someone" "is" "smart" "+")) -> ("someone" "is" "blue" "+"))
White, smart people are big.
((("someone" "is" "white" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "big" "+"))
All green people are furry.
((("someone" "is" "green" "+")) -> ("someone" "is" "furry" "+"))
All big, green people are blue.
((("someone" "is" "big" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "blue" "+"))
Dave is big.
True
1
proof
[(triple1 OR ((triple5 triple4) -> rule4))]
("Dave" "is" "big" "+")
triple1
((triple5 triple4) -> (rule4 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is not blue.
False
1
inv-proof
[(triple2 OR ((triple4) -> rule3) OR ((triple5) -> rule1))]
("Dave" "is" "blue" "-")
triple2
((triple4) -> (rule3 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
((triple5) -> (rule1 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Gary is furry.
True
2
proof
[(((triple6) -> rule5))]
("Gary" "is" "furry" "+")
((triple6) -> (rule5 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is not blue.
False
2
inv-proof
[(((triple7) -> rule3))]
("Gary" "is" "blue" "-")
((triple7) -> (rule3 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is big.
True
4
proof
[(((triple6 ((triple7) -> rule3)) -> rule2))]
("Gary" "is" "big" "+")
((triple6 ((triple7) -> (rule3 % int2))) -> (rule2 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is not big.
False
4
inv-proof
[(((triple6 ((triple7) -> rule3)) -> rule2))]
("Gary" "is" "big" "-")
((triple6 ((triple7) -> (rule3 % int2))) -> (rule2 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Dave is not green.
Unknown
inv-random
[@0: Dave is green.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "green" "-")
Gary is white.
Unknown
random
[@0: Gary is white.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "white" "+")
Dave is not cold.
Unknown
inv-random
[@0: Dave is cold.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "cold" "-")
Gary is cold.
Unknown
random
[@0: Gary is cold.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "cold" "+")
@0: Dave is big.[(triple1 OR ((triple5 triple4) -> rule4))] Dave is blue.[(triple2 OR ((triple4) -> rule3) OR ((triple5) -> rule1))] Dave is furry.[(triple3)] Dave is smart.[(triple4)] Dave is white.[(triple5)] Gary is green.[(triple6)] Gary is smart.[(triple7)] @1: Gary is blue.[(((triple7) -> rule3))] Gary is furry.[(((triple6) -> rule5))] @2: Gary is big.[(((triple6 ((triple7) -> rule3)) -> rule2))]
Dave is big.
("Dave" "is" "big" "+")
triple1
((triple5 triple4) -> (rule4 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
triple2
((triple4) -> (rule3 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
((triple5) -> (rule1 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
triple3
Dave is smart.
("Dave" "is" "smart" "+")
triple4
Dave is white.
("Dave" "is" "white" "+")
triple5
Gary is green.
("Gary" "is" "green" "+")
triple6
Gary is smart.
("Gary" "is" "smart" "+")
triple7
Gary is blue.
("Gary" "is" "blue" "+")
((triple7) -> (rule3 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
((triple6) -> (rule5 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
((triple6 ((triple7) -> (rule3 % int2))) -> (rule2 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2