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