Dave is big. Dave is kind. Dave is quiet. Dave is white. Gary is quiet. Gary is red. Gary is white. All big people are quiet. If someone is young then they are rough. All kind, young people are quiet. All red people are rough. If someone is quiet and big then they are rough. All white, young people are quiet.
Dave is big.
("Dave" "is" "big" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is white.
("Dave" "is" "white" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is white.
("Gary" "is" "white" "+")
All big people are quiet.
((("someone" "is" "big" "+")) -> ("someone" "is" "quiet" "+"))
If someone is young then they are rough.
((("someone" "is" "young" "+")) -> ("someone" "is" "rough" "+"))
All kind, young people are quiet.
((("someone" "is" "kind" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "quiet" "+"))
All red people are rough.
((("someone" "is" "red" "+")) -> ("someone" "is" "rough" "+"))
If someone is quiet and big then they are rough.
((("someone" "is" "quiet" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "rough" "+"))
All white, young people are quiet.
((("someone" "is" "white" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "quiet" "+"))
Dave is quiet.
True
1
proof
[(triple3 OR ((triple1) -> rule1))]
("Dave" "is" "quiet" "+")
triple3
((triple1) -> (rule1 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is not kind.
False
1
inv-proof
[(triple2)]
("Dave" "is" "kind" "-")
triple2
Dave is rough.
True
3
proof
[(((triple3 triple1) -> rule5) OR ((((triple1) -> rule1) triple1) -> rule5))]
("Dave" "is" "rough" "+")
((triple3 triple1) -> (rule5 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
((((triple1) -> (rule1 % int2)) triple1) -> (rule5 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is not rough.
False
3
inv-proof
[(((triple3 triple1) -> rule5) OR ((((triple1) -> rule1) triple1) -> rule5))]
("Dave" "is" "rough" "-")
((triple3 triple1) -> (rule5 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
((((triple1) -> (rule1 % int2)) triple1) -> (rule5 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is not young.
Unknown
inv-random
[@0: Dave is young.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "young" "-")
Gary is kind.
Unknown
random
[@0: Gary is kind.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "kind" "+")
Dave is not red.
Unknown
inv-random
[@0: Dave is red.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "red" "-")
Gary is young.
Unknown
random
[@0: Gary is young.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "young" "+")
@0: Dave is big.[(triple1)] Dave is kind.[(triple2)] Dave is quiet.[(triple3 OR ((triple1) -> rule1))] Dave is white.[(triple4)] Gary is quiet.[(triple5)] Gary is red.[(triple6)] Gary is white.[(triple7)] @1: Dave is rough.[(((triple3 triple1) -> rule5) OR ((((triple1) -> rule1) triple1) -> rule5))] Gary is rough.[(((triple6) -> rule4))]
Dave is big.
("Dave" "is" "big" "+")
triple1
Dave is kind.
("Dave" "is" "kind" "+")
triple2
Dave is quiet.
("Dave" "is" "quiet" "+")
triple3
((triple1) -> (rule1 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
triple4
Gary is quiet.
("Gary" "is" "quiet" "+")
triple5
Gary is red.
("Gary" "is" "red" "+")
triple6
Gary is white.
("Gary" "is" "white" "+")
triple7
Dave is rough.
("Dave" "is" "rough" "+")
((triple3 triple1) -> (rule5 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
((((triple1) -> (rule1 % int2)) triple1) -> (rule5 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
((triple6) -> (rule4 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1