Gary is red. If Gary is blue and Gary is white then Gary is not smart. If Gary is red then Gary is not white. If someone is red and not white then they are rough. All big, smart people are quiet. All rough people are big. All rough, quiet people are big.
Gary is red.
("Gary" "is" "red" "+")
If Gary is blue and Gary is white then Gary is not smart.
((("Gary" "is" "blue" "+") ("Gary" "is" "white" "+")) -> ("Gary" "is" "smart" "-"))
If Gary is red then Gary is not white.
((("Gary" "is" "red" "+")) -> ("Gary" "is" "white" "-"))
If someone is red and not white then they are rough.
((("someone" "is" "red" "+") ("someone" "is" "white" "~")) -> ("someone" "is" "rough" "+"))
All big, smart people are quiet.
((("someone" "is" "big" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "quiet" "+"))
All rough people are big.
((("someone" "is" "rough" "+")) -> ("someone" "is" "big" "+"))
All rough, quiet people are big.
((("someone" "is" "rough" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "big" "+"))
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 not white.
True
2
proof
[(((triple1) -> rule2))]
("Gary" "is" "white" "-")
((triple1) -> (rule2 % int1))
Gary is not white.
("Gary" "is" "white" "-")
int1
Gary is white.
False
2
inv-proof
[(((triple1) -> rule2))]
("Gary" "is" "white" "+")
((triple1) -> (rule2 % int1))
Gary is not white.
("Gary" "is" "white" "-")
int1
Gary is rough.
True
4
proof
[(((triple1 ((triple1) -> rule2)) -> rule3))]
("Gary" "is" "rough" "+")
((triple1 ((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is not white.
("Gary" "is" "white" "-")
int2
Gary is not rough.
False
4
inv-proof
[(((triple1 ((triple1) -> rule2)) -> rule3))]
("Gary" "is" "rough" "-")
((triple1 ((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is not white.
("Gary" "is" "white" "-")
int2
Gary is big.
True
5
proof
[(((((triple1 ((triple1) -> rule2)) -> rule3)) -> rule5))]
("Gary" "is" "big" "+")
((((triple1 ((triple1) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is not white.
("Gary" "is" "white" "-")
int3
Gary is not big.
False
5
inv-proof
[(((((triple1 ((triple1) -> rule2)) -> rule3)) -> rule5))]
("Gary" "is" "big" "-")
((((triple1 ((triple1) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is not white.
("Gary" "is" "white" "-")
int3
Gary is not quiet.
Unknown
inv-rconc
[@1: Gary is quiet.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Gary" "is" "quiet" "-")
Gary is blue.
Unknown
random
[@0: Gary is blue.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "blue" "+")
@0: Gary is red.[(triple1)] @1: Gary is not white.[(((triple1) -> rule2))] @2: Gary is rough.[(((triple1 ((triple1) -> rule2)) -> rule3))] @3: Gary is big.[(((((triple1 ((triple1) -> rule2)) -> rule3)) -> rule5))]
Gary is red.
("Gary" "is" "red" "+")
triple1
Gary is not white.
("Gary" "is" "white" "-")
((triple1) -> (rule2 % int1))
Gary is not white.
("Gary" "is" "white" "-")
int1
Gary is rough.
("Gary" "is" "rough" "+")
((triple1 ((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is not white.
("Gary" "is" "white" "-")
int2
Gary is big.
("Gary" "is" "big" "+")
((((triple1 ((triple1) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is not white.
("Gary" "is" "white" "-")
int3