Anne is smart. Gary is round. If someone is rough and not big then they are smart. If Gary is rough and Gary is red then Gary is smart. If someone is round then they are white. If someone is rough and smart then they are red. Smart people are green. If someone is smart and green then they are not round.
Anne is smart.
("Anne" "is" "smart" "+")
Gary is round.
("Gary" "is" "round" "+")
If someone is rough and not big then they are smart.
((("someone" "is" "rough" "+") ("someone" "is" "big" "~")) -> ("someone" "is" "smart" "+"))
If Gary is rough and Gary is red then Gary is smart.
((("Gary" "is" "rough" "+") ("Gary" "is" "red" "+")) -> ("Gary" "is" "smart" "+"))
If someone is round then they are white.
((("someone" "is" "round" "+")) -> ("someone" "is" "white" "+"))
If someone is rough and smart then they are red.
((("someone" "is" "rough" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "red" "+"))
Smart people are green.
((("someone" "is" "smart" "+")) -> ("someone" "is" "green" "+"))
If someone is smart and green then they are not round.
((("someone" "is" "smart" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "round" "-"))
Gary is round.
True
1
proof
[(triple2)]
("Gary" "is" "round" "+")
triple2
Gary is not round.
False
1
inv-proof
[(triple2)]
("Gary" "is" "round" "-")
triple2
Gary is white.
True
2
proof
[(((triple2) -> rule3))]
("Gary" "is" "white" "+")
((triple2) -> (rule3 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Anne is not green.
False
2
inv-proof
[(((triple1) -> rule5))]
("Anne" "is" "green" "-")
((triple1) -> (rule5 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is not round.
True
4
proof
[(((triple1 ((triple1) -> rule5)) -> rule6))]
("Anne" "is" "round" "-")
((triple1 ((triple1) -> (rule5 % int2))) -> (rule6 % int1))
Anne is not round.
("Anne" "is" "round" "-")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is round.
False
4
inv-proof
[(((triple1 ((triple1) -> rule5)) -> rule6))]
("Anne" "is" "round" "+")
((triple1 ((triple1) -> (rule5 % int2))) -> (rule6 % int1))
Anne is not round.
("Anne" "is" "round" "-")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Gary is not green.
Unknown
inv-rconc
[@2: Gary is green.[CWA. Example of deepest failure = (rule5 <- rule1 <- FAIL)]]
("Gary" "is" "green" "-")
Anne is white.
Unknown
rconc
[@1: Anne is white.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Anne" "is" "white" "+")
Gary is not smart.
Unknown
inv-rconc
[@1: Gary is smart.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "smart" "-")
Anne is rough.
Unknown
random
[@0: Anne is rough.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "rough" "+")
Gary is not rough.
Unknown
inv-random
[@0: Gary is rough.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "rough" "-")
Gary is big.
Unknown
random
[@0: Gary is big.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "big" "+")
@0: Anne is smart.[(triple1)] Gary is round.[(triple2)] @1: Anne is green.[(((triple1) -> rule5))] Gary is white.[(((triple2) -> rule3))] @2: Anne is not round.[(((triple1 ((triple1) -> rule5)) -> rule6))]
Anne is smart.
("Anne" "is" "smart" "+")
triple1
Gary is round.
("Gary" "is" "round" "+")
triple2
Anne is green.
("Anne" "is" "green" "+")
((triple1) -> (rule5 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
((triple2) -> (rule3 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Anne is not round.
("Anne" "is" "round" "-")
((triple1 ((triple1) -> (rule5 % int2))) -> (rule6 % int1))
Anne is not round.
("Anne" "is" "round" "-")
int1
Anne is green.
("Anne" "is" "green" "+")
int2