Anne is nice. Anne is red. Gary is red. If Gary is cold and Gary is nice then Gary is rough. All furry things are big. If something is big then it is rough. Quiet, cold things are rough. All big, rough things are cold. If something is rough then it is nice. All nice things are big. All big things are furry.
Anne is nice.
("Anne" "is" "nice" "+")
Anne is red.
("Anne" "is" "red" "+")
Gary is red.
("Gary" "is" "red" "+")
If Gary is cold and Gary is nice then Gary is rough.
((("Gary" "is" "cold" "+") ("Gary" "is" "nice" "+")) -> ("Gary" "is" "rough" "+"))
All furry things are big.
((("something" "is" "furry" "+")) -> ("something" "is" "big" "+"))
If something is big then it is rough.
((("something" "is" "big" "+")) -> ("something" "is" "rough" "+"))
Quiet, cold things are rough.
((("something" "is" "quiet" "+") ("something" "is" "cold" "+")) -> ("something" "is" "rough" "+"))
All big, rough things are cold.
((("something" "is" "big" "+") ("something" "is" "rough" "+")) -> ("something" "is" "cold" "+"))
If something is rough then it is nice.
((("something" "is" "rough" "+")) -> ("something" "is" "nice" "+"))
All nice things are big.
((("something" "is" "nice" "+")) -> ("something" "is" "big" "+"))
All big things are furry.
((("something" "is" "big" "+")) -> ("something" "is" "furry" "+"))
Anne is nice.
True
1
proof
[(triple1)]
("Anne" "is" "nice" "+")
triple1
Anne is not nice.
False
1
inv-proof
[(triple1)]
("Anne" "is" "nice" "-")
triple1
Anne is big.
True
2
proof
[(((triple1) -> rule7))]
("Anne" "is" "big" "+")
((triple1) -> (rule7 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is not big.
False
2
inv-proof
[(((triple1) -> rule7))]
("Anne" "is" "big" "-")
((triple1) -> (rule7 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Gary is not nice.
Unknown
inv-rconc
[@5: Gary is nice.[CWA. Example of deepest failure = (rule6 <- rule3 <- rule2 <- rule8 <- rule7 <- FAIL)]]
("Gary" "is" "nice" "-")
Gary is big.
Unknown
rconc
[@5: Gary is big.[CWA. Example of deepest failure = (rule2 <- rule8 <- rule7 <- rule6 <- rule1 <- FAIL)]]
("Gary" "is" "big" "+")
Anne is not quiet.
Unknown
inv-random
[@0: Anne is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "quiet" "-")
Gary is quiet.
Unknown
random
[@0: Gary is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "quiet" "+")
@0: Anne is nice.[(triple1)] Anne is red.[(triple2)] Gary is red.[(triple3)] @1: Anne is big.[(((triple1) -> rule7))] @2: Anne is furry.[(((((triple1) -> rule7)) -> rule8))] Anne is rough.[(((((triple1) -> rule7)) -> rule3))] @3: Anne is cold.[(((((triple1) -> rule7) ((((triple1) -> rule7)) -> rule3)) -> rule5))]
Anne is nice.
("Anne" "is" "nice" "+")
triple1
Anne is red.
("Anne" "is" "red" "+")
triple2
Gary is red.
("Gary" "is" "red" "+")
triple3
Anne is big.
("Anne" "is" "big" "+")
((triple1) -> (rule7 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
((((triple1) -> (rule7 % int2))) -> (rule8 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
((((triple1) -> (rule7 % int2))) -> (rule3 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
((((triple1) -> (rule7 % int3)) ((((triple1) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
int3