Anne is green. Gary is not smart. If something is smart then it is not round. If something is round then it is not white. White things are cold. If Gary is white then Gary is green. If Anne is green then Anne is round. All round, white things are green. If something is round and not white then it is big. If Gary is not green then Gary is cold.
Anne is green.
("Anne" "is" "green" "+")
Gary is not smart.
("Gary" "is" "smart" "-")
If something is smart then it is not round.
((("something" "is" "smart" "+")) -> ("something" "is" "round" "-"))
If something is round then it is not white.
((("something" "is" "round" "+")) -> ("something" "is" "white" "-"))
White things are cold.
((("something" "is" "white" "+")) -> ("something" "is" "cold" "+"))
If Gary is white then Gary is green.
((("Gary" "is" "white" "+")) -> ("Gary" "is" "green" "+"))
If Anne is green then Anne is round.
((("Anne" "is" "green" "+")) -> ("Anne" "is" "round" "+"))
All round, white things are green.
((("something" "is" "round" "+") ("something" "is" "white" "+")) -> ("something" "is" "green" "+"))
If something is round and not white then it is big.
((("something" "is" "round" "+") ("something" "is" "white" "~")) -> ("something" "is" "big" "+"))
If Gary is not green then Gary is cold.
((("Gary" "is" "green" "~")) -> ("Gary" "is" "cold" "+"))
Gary is not smart.
True
1
proof
[(triple2)]
("Gary" "is" "smart" "-")
triple2
Anne is not green.
False
1
inv-proof
[(triple1)]
("Anne" "is" "green" "-")
triple1
Anne is round.
True
2
proof
[(((triple1) -> rule5))]
("Anne" "is" "round" "+")
((triple1) -> (rule5 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is not round.
False
2
inv-proof
[(((triple1) -> rule5))]
("Anne" "is" "round" "-")
((triple1) -> (rule5 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is not white.
True
3
proof
[(((((triple1) -> rule5)) -> rule2))]
("Anne" "is" "white" "-")
((((triple1) -> (rule5 % int2))) -> (rule2 % int1))
Anne is not white.
("Anne" "is" "white" "-")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is white.
False
3
inv-proof
[(((((triple1) -> rule5)) -> rule2))]
("Anne" "is" "white" "+")
((((triple1) -> (rule5 % int2))) -> (rule2 % int1))
Anne is not white.
("Anne" "is" "white" "-")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is big.
True
6
proof
[(((((triple1) -> rule5) ((((triple1) -> rule5)) -> rule2)) -> rule7))]
("Anne" "is" "big" "+")
((((triple1) -> (rule5 % int3)) ((((triple1) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is not white.
("Anne" "is" "white" "-")
int2
Anne is round.
("Anne" "is" "round" "+")
int3
Anne is not big.
False
6
inv-proof
[(((((triple1) -> rule5) ((((triple1) -> rule5)) -> rule2)) -> rule7))]
("Anne" "is" "big" "-")
((((triple1) -> (rule5 % int3)) ((((triple1) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is not white.
("Anne" "is" "white" "-")
int2
Anne is round.
("Anne" "is" "round" "+")
int3
Gary is not cold.
Unknown
inv-rconc
[@1: Gary is cold.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Gary" "is" "cold" "-")
Anne is cold.
Unknown
rconc
[@1: Anne is cold.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Anne" "is" "cold" "+")
Gary is not big.
Unknown
inv-rconc
[@1: Gary is big.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Gary" "is" "big" "-")
Gary is green.
Unknown
rconc
[@1: Gary is green.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Gary" "is" "green" "+")
Gary is not round.
Unknown
inv-random
[@0: Gary is round.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "round" "-")
Anne is young.
Unknown
random
[@0: Anne is young.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "young" "+")
Gary is not white.
Unknown
inv-random
[@0: Gary is white.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "white" "-")
Anne is smart.
Unknown
random
[@0: Anne is smart.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "smart" "+")
@0: Anne is green.[(triple1)] Gary is not smart.[(triple2)] @1: Anne is round.[(((triple1) -> rule5))] @2: Anne is not white.[(((((triple1) -> rule5)) -> rule2))] @3: Anne is big.[(((((triple1) -> rule5) ((((triple1) -> rule5)) -> rule2)) -> rule7))]
Anne is green.
("Anne" "is" "green" "+")
triple1
Gary is not smart.
("Gary" "is" "smart" "-")
triple2
Anne is round.
("Anne" "is" "round" "+")
((triple1) -> (rule5 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is not white.
("Anne" "is" "white" "-")
((((triple1) -> (rule5 % int2))) -> (rule2 % int1))
Anne is not white.
("Anne" "is" "white" "-")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
((((triple1) -> (rule5 % int3)) ((((triple1) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is not white.
("Anne" "is" "white" "-")
int2
Anne is round.
("Anne" "is" "round" "+")
int3