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