Gary is red. If someone is kind then they are red. All white, rough people are kind. All rough people are quiet. If someone is rough and white then they are big. If someone is red then they are rough. If someone is quiet and rough then they are kind.
Gary is red.
("Gary" "is" "red" "+")
If someone is kind then they are red.
((("someone" "is" "kind" "+")) -> ("someone" "is" "red" "+"))
All white, rough people are kind.
((("someone" "is" "white" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "kind" "+"))
All rough people are quiet.
((("someone" "is" "rough" "+")) -> ("someone" "is" "quiet" "+"))
If someone is rough and white then they are big.
((("someone" "is" "rough" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "big" "+"))
If someone is red then they are rough.
((("someone" "is" "red" "+")) -> ("someone" "is" "rough" "+"))
If someone is quiet and rough then they are kind.
((("someone" "is" "quiet" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "kind" "+"))
Gary is red.
True
1
proof
[(triple1)]
("Gary" "is" "red" "+")
triple1
Gary is not red.
False
1
inv-proof
[(triple1)]
("Gary" "is" "red" "-")
triple1
Gary is rough.
True
2
proof
[(((triple1) -> rule5))]
("Gary" "is" "rough" "+")
((triple1) -> (rule5 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is not rough.
False
2
inv-proof
[(((triple1) -> rule5))]
("Gary" "is" "rough" "-")
((triple1) -> (rule5 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is quiet.
True
3
proof
[(((((triple1) -> rule5)) -> rule3))]
("Gary" "is" "quiet" "+")
((((triple1) -> (rule5 % int2))) -> (rule3 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is not quiet.
False
3
inv-proof
[(((((triple1) -> rule5)) -> rule3))]
("Gary" "is" "quiet" "-")
((((triple1) -> (rule5 % int2))) -> (rule3 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is kind.
True
6
proof
[(((((((triple1) -> rule5)) -> rule3) ((triple1) -> rule5)) -> rule6))]
("Gary" "is" "kind" "+")
((((((triple1) -> (rule5 % int3))) -> (rule3 % int2)) ((triple1) -> (rule5 % int3))) -> (rule6 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
Gary is not kind.
False
6
inv-proof
[(((((((triple1) -> rule5)) -> rule3) ((triple1) -> rule5)) -> rule6))]
("Gary" "is" "kind" "-")
((((((triple1) -> (rule5 % int3))) -> (rule3 % int2)) ((triple1) -> (rule5 % int3))) -> (rule6 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
Gary is not big.
Unknown
inv-rconc
[@1: Gary is big.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Gary" "is" "big" "-")
Gary is nice.
Unknown
random
[@0: Gary is nice.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "nice" "+")
@0: Gary is red.[(triple1)] @1: Gary is rough.[(((triple1) -> rule5))] @2: Gary is quiet.[(((((triple1) -> rule5)) -> rule3))] @3: Gary is kind.[(((((((triple1) -> rule5)) -> rule3) ((triple1) -> rule5)) -> rule6))]
Gary is red.
("Gary" "is" "red" "+")
triple1
Gary is rough.
("Gary" "is" "rough" "+")
((triple1) -> (rule5 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
((((triple1) -> (rule5 % int2))) -> (rule3 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
((((((triple1) -> (rule5 % int3))) -> (rule3 % int2)) ((triple1) -> (rule5 % int3))) -> (rule6 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3