Dave is green. Dave is kind. Dave is quiet. Dave is smart. Gary is big. Gary is blue. Gary is green. Gary is quiet. Gary is rough. Gary is smart. If Dave is green and Dave is kind then Dave is blue. Blue things are green. If Gary is blue then Gary is quiet. If something is kind and smart then it is green. If Dave is blue then Dave is smart. If Gary is big and Gary is rough then Gary is green. If Gary is green then Gary is smart. If Gary is smart and Gary is blue then Gary is big.
Dave is green.
("Dave" "is" "green" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is smart.
("Gary" "is" "smart" "+")
If Dave is green and Dave is kind then Dave is blue.
((("Dave" "is" "green" "+") ("Dave" "is" "kind" "+")) -> ("Dave" "is" "blue" "+"))
Blue things are green.
((("something" "is" "blue" "+")) -> ("something" "is" "green" "+"))
If Gary is blue then Gary is quiet.
((("Gary" "is" "blue" "+")) -> ("Gary" "is" "quiet" "+"))
If something is kind and smart then it is green.
((("something" "is" "kind" "+") ("something" "is" "smart" "+")) -> ("something" "is" "green" "+"))
If Dave is blue then Dave is smart.
((("Dave" "is" "blue" "+")) -> ("Dave" "is" "smart" "+"))
If Gary is big and Gary is rough then Gary is green.
((("Gary" "is" "big" "+") ("Gary" "is" "rough" "+")) -> ("Gary" "is" "green" "+"))
If Gary is green then Gary is smart.
((("Gary" "is" "green" "+")) -> ("Gary" "is" "smart" "+"))
If Gary is smart and Gary is blue then Gary is big.
((("Gary" "is" "smart" "+") ("Gary" "is" "blue" "+")) -> ("Gary" "is" "big" "+"))
Dave is kind.
True
1
proof
[(triple2)]
("Dave" "is" "kind" "+")
triple2
Dave is not kind.
False
1
inv-proof
[(triple2)]
("Dave" "is" "kind" "-")
triple2
Dave is blue.
True
3
proof
[(((triple1 triple2) -> rule1) OR ((((triple2 triple4) -> rule4) triple2) -> rule1))]
("Dave" "is" "blue" "+")
((triple1 triple2) -> (rule1 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
((((triple2 triple4) -> (rule4 % int2)) triple2) -> (rule1 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is not blue.
False
3
inv-proof
[(((triple1 triple2) -> rule1) OR ((((triple2 triple4) -> rule4) triple2) -> rule1))]
("Dave" "is" "blue" "-")
((triple1 triple2) -> (rule1 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
((((triple2 triple4) -> (rule4 % int2)) triple2) -> (rule1 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is not rough.
Unknown
inv-random
[@0: Dave is rough.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "rough" "-")
Gary is kind.
Unknown
random
[@0: Gary is kind.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "kind" "+")
@0: Dave is green.[(triple1 OR ((triple2 triple4) -> rule4))] Dave is kind.[(triple2)] Dave is quiet.[(triple3)] Dave is smart.[(triple4 OR ((((triple1 triple2) -> rule1)) -> rule5))] Gary is big.[(triple5 OR ((triple10 triple6) -> rule8) OR ((((triple7) -> rule7) triple6) -> rule8) OR ((((((triple6) -> rule2)) -> rule7) triple6) -> rule8))] Gary is blue.[(triple6)] Gary is green.[(triple7 OR ((triple6) -> rule2) OR ((triple5 triple9) -> rule6) OR ((((triple10 triple6) -> rule8) triple9) -> rule6))] Gary is quiet.[(triple8 OR ((triple6) -> rule3))] Gary is rough.[(triple9)] Gary is smart.[(triple10 OR ((triple7) -> rule7) OR ((((triple6) -> rule2)) -> rule7) OR ((((triple5 triple9) -> rule6)) -> rule7))] @1: Dave is blue.[(((triple1 triple2) -> rule1) OR ((((triple2 triple4) -> rule4) triple2) -> rule1))]
Dave is green.
("Dave" "is" "green" "+")
triple1
((triple2 triple4) -> (rule4 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
triple2
Dave is quiet.
("Dave" "is" "quiet" "+")
triple3
Dave is smart.
("Dave" "is" "smart" "+")
triple4
((((triple1 triple2) -> (rule1 % int2))) -> (rule5 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
triple5
((triple10 triple6) -> (rule8 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
((((triple7) -> (rule7 % int2)) triple6) -> (rule8 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
((((((triple6) -> (rule2 % int3))) -> (rule7 % int2)) triple6) -> (rule8 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3
Gary is blue.
("Gary" "is" "blue" "+")
triple6
Gary is green.
("Gary" "is" "green" "+")
triple7
((triple6) -> (rule2 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
((triple5 triple9) -> (rule6 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
((((triple10 triple6) -> (rule8 % int2)) triple9) -> (rule6 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
triple8
((triple6) -> (rule3 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
triple9
Gary is smart.
("Gary" "is" "smart" "+")
triple10
((triple7) -> (rule7 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
((((triple6) -> (rule2 % int2))) -> (rule7 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
((((triple5 triple9) -> (rule6 % int2))) -> (rule7 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
((triple1 triple2) -> (rule1 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
((((triple2 triple4) -> (rule4 % int2)) triple2) -> (rule1 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2