Charlie is quiet. Charlie is red. Charlie is round. Gary is green. Gary is kind. Gary is quiet. Gary is rough. If someone is quiet and green then they are red. Big people are red. If someone is red and kind then they are round.
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is rough.
("Gary" "is" "rough" "+")
If someone is quiet and green then they are red.
((("someone" "is" "quiet" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "red" "+"))
Big people are red.
((("someone" "is" "big" "+")) -> ("someone" "is" "red" "+"))
If someone is red and kind then they are round.
((("someone" "is" "red" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "round" "+"))
Gary is kind.
True
1
proof
[(triple5)]
("Gary" "is" "kind" "+")
triple5
Gary is not quiet.
False
1
inv-proof
[(triple6)]
("Gary" "is" "quiet" "-")
triple6
Gary is red.
True
3
proof
[(((triple6 triple4) -> rule1))]
("Gary" "is" "red" "+")
((triple6 triple4) -> (rule1 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is not red.
False
3
inv-proof
[(((triple6 triple4) -> rule1))]
("Gary" "is" "red" "-")
((triple6 triple4) -> (rule1 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is round.
True
5
proof
[(((((triple6 triple4) -> rule1) triple5) -> rule3))]
("Gary" "is" "round" "+")
((((triple6 triple4) -> (rule1 % int2)) triple5) -> (rule3 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is not round.
False
5
inv-proof
[(((((triple6 triple4) -> rule1) triple5) -> rule3))]
("Gary" "is" "round" "-")
((((triple6 triple4) -> (rule1 % int2)) triple5) -> (rule3 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Charlie is not big.
Unknown
inv-random
[@0: Charlie is big.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "big" "-")
Charlie is rough.
Unknown
random
[@0: Charlie is rough.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "rough" "+")
Charlie is not green.
Unknown
inv-random
[@0: Charlie is green.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "green" "-")
Gary is big.
Unknown
random
[@0: Gary is big.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "big" "+")
@0: Charlie is quiet.[(triple1)] Charlie is red.[(triple2)] Charlie is round.[(triple3)] Gary is green.[(triple4)] Gary is kind.[(triple5)] Gary is quiet.[(triple6)] Gary is rough.[(triple7)] @1: Gary is red.[(((triple6 triple4) -> rule1))] @2: Gary is round.[(((((triple6 triple4) -> rule1) triple5) -> rule3))]
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple1
Charlie is red.
("Charlie" "is" "red" "+")
triple2
Charlie is round.
("Charlie" "is" "round" "+")
triple3
Gary is green.
("Gary" "is" "green" "+")
triple4
Gary is kind.
("Gary" "is" "kind" "+")
triple5
Gary is quiet.
("Gary" "is" "quiet" "+")
triple6
Gary is rough.
("Gary" "is" "rough" "+")
triple7
Gary is red.
("Gary" "is" "red" "+")
((triple6 triple4) -> (rule1 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
((((triple6 triple4) -> (rule1 % int2)) triple5) -> (rule3 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2