Dave is kind. Dave is young. Gary is kind. If Gary is big then Gary is blue. If someone is quiet and young then they are not red. Quiet people are big. If someone is blue then they are quiet. If someone is kind then they are blue. Red, young people are kind. All rough people are kind. If someone is kind and blue then they are rough.
Dave is kind.
("Dave" "is" "kind" "+")
Dave is young.
("Dave" "is" "young" "+")
Gary is kind.
("Gary" "is" "kind" "+")
If Gary is big then Gary is blue.
((("Gary" "is" "big" "+")) -> ("Gary" "is" "blue" "+"))
If someone is quiet and young then they are not red.
((("someone" "is" "quiet" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "red" "-"))
Quiet people are big.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "big" "+"))
If someone is blue then they are quiet.
((("someone" "is" "blue" "+")) -> ("someone" "is" "quiet" "+"))
If someone is kind then they are blue.
((("someone" "is" "kind" "+")) -> ("someone" "is" "blue" "+"))
Red, young people are kind.
((("someone" "is" "red" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "kind" "+"))
All rough people are kind.
((("someone" "is" "rough" "+")) -> ("someone" "is" "kind" "+"))
If someone is kind and blue then they are rough.
((("someone" "is" "kind" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "rough" "+"))
Dave is young.
True
1
proof
[(triple2)]
("Dave" "is" "young" "+")
triple2
Dave is not kind.
False
1
inv-proof
[(triple1)]
("Dave" "is" "kind" "-")
triple1
Gary is blue.
True
2
proof
[(((triple3) -> rule5))]
("Gary" "is" "blue" "+")
((triple3) -> (rule5 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is not blue.
False
2
inv-proof
[(((triple3) -> rule5))]
("Gary" "is" "blue" "-")
((triple3) -> (rule5 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is rough.
True
4
proof
[(((triple3 ((triple3) -> rule5)) -> rule8))]
("Gary" "is" "rough" "+")
((triple3 ((triple3) -> (rule5 % int2))) -> (rule8 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Dave is not rough.
False
4
inv-proof
[(((triple1 ((triple1) -> rule5)) -> rule8))]
("Dave" "is" "rough" "-")
((triple1 ((triple1) -> (rule5 % int2))) -> (rule8 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is not red.
True
5
proof
[(((((((triple1) -> rule5)) -> rule4) triple2) -> rule2))]
("Dave" "is" "red" "-")
((((((triple1) -> (rule5 % int3))) -> (rule4 % int2)) triple2) -> (rule2 % int1))
Dave is not red.
("Dave" "is" "red" "-")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
Dave is red.
False
5
inv-proof
[(((((((triple1) -> rule5)) -> rule4) triple2) -> rule2))]
("Dave" "is" "red" "+")
((((((triple1) -> (rule5 % int3))) -> (rule4 % int2)) triple2) -> (rule2 % int1))
Dave is not red.
("Dave" "is" "red" "-")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
Gary is not red.
Unknown
inv-random
[@0: Gary is red.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "red" "-")
Gary is young.
Unknown
random
[@0: Gary is young.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "young" "+")
@0: Dave is kind.[(triple1)] Dave is young.[(triple2)] Gary is kind.[(triple3)] @1: Dave is blue.[(((triple1) -> rule5))] Gary is blue.[(((triple3) -> rule5))] @2: Dave is quiet.[(((((triple1) -> rule5)) -> rule4))] Dave is rough.[(((triple1 ((triple1) -> rule5)) -> rule8))] Gary is quiet.[(((((triple3) -> rule5)) -> rule4))] Gary is rough.[(((triple3 ((triple3) -> rule5)) -> rule8))] @3: Dave is big.[(((((((triple1) -> rule5)) -> rule4)) -> rule3))] Dave is not red.[(((((((triple1) -> rule5)) -> rule4) triple2) -> rule2))] Gary is big.[(((((((triple3) -> rule5)) -> rule4)) -> rule3))]
Dave is kind.
("Dave" "is" "kind" "+")
triple1
Dave is young.
("Dave" "is" "young" "+")
triple2
Gary is kind.
("Gary" "is" "kind" "+")
triple3
Dave is blue.
("Dave" "is" "blue" "+")
((triple1) -> (rule5 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
((triple3) -> (rule5 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
((((triple1) -> (rule5 % int2))) -> (rule4 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
((triple1 ((triple1) -> (rule5 % int2))) -> (rule8 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
((((triple3) -> (rule5 % int2))) -> (rule4 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
((triple3 ((triple3) -> (rule5 % int2))) -> (rule8 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
((((((triple1) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
Dave is not red.
("Dave" "is" "red" "-")
((((((triple1) -> (rule5 % int3))) -> (rule4 % int2)) triple2) -> (rule2 % int1))
Dave is not red.
("Dave" "is" "red" "-")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
Gary is big.
("Gary" "is" "big" "+")
((((((triple3) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3