Dave is cold. Dave is kind. Dave is nice. Gary is cold. Gary is kind. Gary is red. Gary is young. If something is young and smart then it is kind. Rough things are red. If something is kind and nice then it is red. All red things are rough. All cold things are nice. Nice, kind things are young. If Dave is young and Dave is red then Dave is kind. If something is cold then it is kind.
Dave is cold.
("Dave" "is" "cold" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is young.
("Gary" "is" "young" "+")
If something is young and smart then it is kind.
((("something" "is" "young" "+") ("something" "is" "smart" "+")) -> ("something" "is" "kind" "+"))
Rough things are red.
((("something" "is" "rough" "+")) -> ("something" "is" "red" "+"))
If something is kind and nice then it is red.
((("something" "is" "kind" "+") ("something" "is" "nice" "+")) -> ("something" "is" "red" "+"))
All red things are rough.
((("something" "is" "red" "+")) -> ("something" "is" "rough" "+"))
All cold things are nice.
((("something" "is" "cold" "+")) -> ("something" "is" "nice" "+"))
Nice, kind things are young.
((("something" "is" "nice" "+") ("something" "is" "kind" "+")) -> ("something" "is" "young" "+"))
If Dave is young and Dave is red then Dave is kind.
((("Dave" "is" "young" "+") ("Dave" "is" "red" "+")) -> ("Dave" "is" "kind" "+"))
If something is cold then it is kind.
((("something" "is" "cold" "+")) -> ("something" "is" "kind" "+"))
Dave is kind.
True
1
proof
[(triple2 OR ((triple1) -> rule8))]
("Dave" "is" "kind" "+")
triple2
((triple1) -> (rule8 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is not nice.
False
1
inv-proof
[(triple3 OR ((triple1) -> rule5))]
("Dave" "is" "nice" "-")
triple3
((triple1) -> (rule5 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Gary is rough.
True
2
proof
[(((triple6) -> rule4) OR ((((triple5 ((triple4) -> rule5)) -> rule3)) -> rule4) OR ((((((triple4) -> rule8) ((triple4) -> rule5)) -> rule3)) -> rule4))]
("Gary" "is" "rough" "+")
((triple6) -> (rule4 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
((((triple5 ((triple4) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3
((((((triple4) -> (rule8 % int4)) ((triple4) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3
Gary is kind.
("Gary" "is" "kind" "+")
int4
Dave is not young.
False
3
inv-proof
[(((triple3 triple2) -> rule6) OR ((triple3 ((triple1) -> rule8)) -> rule6) OR ((((triple1) -> rule5) triple2) -> rule6) OR ((((triple1) -> rule5) ((triple1) -> rule8)) -> rule6))]
("Dave" "is" "young" "-")
((triple3 triple2) -> (rule6 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
((triple3 ((triple1) -> (rule8 % int2))) -> (rule6 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
((((triple1) -> (rule5 % int2)) triple2) -> (rule6 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
((((triple1) -> (rule5 % int3)) ((triple1) -> (rule8 % int2))) -> (rule6 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Gary is not smart.
Unknown
inv-random
[@0: Gary is smart.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "smart" "-")
Dave is smart.
Unknown
random
[@0: Dave is smart.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "smart" "+")
@0: Dave is cold.[(triple1)] Dave is kind.[(triple2 OR ((triple1) -> rule8))] Dave is nice.[(triple3 OR ((triple1) -> rule5))] Gary is cold.[(triple4)] Gary is kind.[(triple5 OR ((triple4) -> rule8))] Gary is red.[(triple6 OR ((triple5 ((triple4) -> rule5)) -> rule3) OR ((((triple4) -> rule8) ((triple4) -> rule5)) -> rule3))] Gary is young.[(triple7 OR ((((triple4) -> rule5) triple5) -> rule6) OR ((((triple4) -> rule5) ((triple4) -> rule8)) -> rule6))] @1: Dave is red.[(((triple2 triple3) -> rule3) OR ((triple2 ((triple1) -> rule5)) -> rule3) OR ((((triple1) -> rule8) triple3) -> rule3) OR ((((triple1) -> rule8) ((triple1) -> rule5)) -> rule3))] Dave is young.[(((triple3 triple2) -> rule6) OR ((triple3 ((triple1) -> rule8)) -> rule6) OR ((((triple1) -> rule5) triple2) -> rule6) OR ((((triple1) -> rule5) ((triple1) -> rule8)) -> rule6))] Gary is nice.[(((triple4) -> rule5))] Gary is rough.[(((triple6) -> rule4) OR ((((triple5 ((triple4) -> rule5)) -> rule3)) -> rule4) OR ((((((triple4) -> rule8) ((triple4) -> rule5)) -> rule3)) -> rule4))] @2: Dave is rough.[(((((triple2 triple3) -> rule3)) -> rule4) OR ((((triple2 ((triple1) -> rule5)) -> rule3)) -> rule4) OR ((((((triple1) -> rule8) triple3) -> rule3)) -> rule4) OR ((((((triple1) -> rule8) ((triple1) -> rule5)) -> rule3)) -> rule4))]
Dave is cold.
("Dave" "is" "cold" "+")
triple1
Dave is kind.
("Dave" "is" "kind" "+")
triple2
((triple1) -> (rule8 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
triple3
((triple1) -> (rule5 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
triple4
Gary is kind.
("Gary" "is" "kind" "+")
triple5
((triple4) -> (rule8 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
triple6
((triple5 ((triple4) -> (rule5 % int2))) -> (rule3 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
((((triple4) -> (rule8 % int3)) ((triple4) -> (rule5 % int2))) -> (rule3 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
int3
Gary is young.
("Gary" "is" "young" "+")
triple7
((((triple4) -> (rule5 % int2)) triple5) -> (rule6 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
((((triple4) -> (rule5 % int3)) ((triple4) -> (rule8 % int2))) -> (rule6 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3
Dave is red.
("Dave" "is" "red" "+")
((triple2 triple3) -> (rule3 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
((triple2 ((triple1) -> (rule5 % int2))) -> (rule3 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
((((triple1) -> (rule8 % int2)) triple3) -> (rule3 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
((((triple1) -> (rule8 % int3)) ((triple1) -> (rule5 % int2))) -> (rule3 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
Dave is young.
("Dave" "is" "young" "+")
((triple3 triple2) -> (rule6 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
((triple3 ((triple1) -> (rule8 % int2))) -> (rule6 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
((((triple1) -> (rule5 % int2)) triple2) -> (rule6 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
((((triple1) -> (rule5 % int3)) ((triple1) -> (rule8 % int2))) -> (rule6 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Gary is nice.
("Gary" "is" "nice" "+")
((triple4) -> (rule5 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
((triple6) -> (rule4 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
((((triple5 ((triple4) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3
((((((triple4) -> (rule8 % int4)) ((triple4) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3
Gary is kind.
("Gary" "is" "kind" "+")
int4
Dave is rough.
("Dave" "is" "rough" "+")
((((triple2 triple3) -> (rule3 % int2))) -> (rule4 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
((((triple2 ((triple1) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
((((((triple1) -> (rule8 % int3)) triple3) -> (rule3 % int2))) -> (rule4 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
((((((triple1) -> (rule8 % int4)) ((triple1) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Dave is kind.
("Dave" "is" "kind" "+")
int4