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