Anne is big. Anne is green. Anne is quiet. Anne is not round. Bob is cold. Bob is round. Charlie is not cold. If Charlie is green and Charlie is cold then Charlie is not big. Smart, cold things are quiet. All round, smart things are not cold. Big things are not cold. All round things are furry. If Anne is big and Anne is not cold then Anne is furry.
Anne is big.
("Anne" "is" "big" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is not round.
("Anne" "is" "round" "-")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is round.
("Bob" "is" "round" "+")
Charlie is not cold.
("Charlie" "is" "cold" "-")
If Charlie is green and Charlie is cold then Charlie is not big.
((("Charlie" "is" "green" "+") ("Charlie" "is" "cold" "+")) -> ("Charlie" "is" "big" "-"))
Smart, cold things are quiet.
((("something" "is" "smart" "+") ("something" "is" "cold" "+")) -> ("something" "is" "quiet" "+"))
All round, smart things are not cold.
((("something" "is" "round" "+") ("something" "is" "smart" "+")) -> ("something" "is" "cold" "-"))
Big things are not cold.
((("something" "is" "big" "+")) -> ("something" "is" "cold" "-"))
All round things are furry.
((("something" "is" "round" "+")) -> ("something" "is" "furry" "+"))
If Anne is big and Anne is not cold then Anne is furry.
((("Anne" "is" "big" "+") ("Anne" "is" "cold" "~")) -> ("Anne" "is" "furry" "+"))
Anne is big.
True
1
proof
[(triple1)]
("Anne" "is" "big" "+")
triple1
Charlie is cold.
False
1
inv-proof
[(triple7)]
("Charlie" "is" "cold" "+")
triple7
Bob is furry.
True
2
proof
[(((triple6) -> rule5))]
("Bob" "is" "furry" "+")
((triple6) -> (rule5 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is not furry.
False
2
inv-proof
[(((triple6) -> rule5))]
("Bob" "is" "furry" "-")
((triple6) -> (rule5 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Anne is furry.
True
4
proof
[(((triple1 ((triple1) -> rule4)) -> rule6))]
("Anne" "is" "furry" "+")
((triple1 ((triple1) -> (rule4 % int2))) -> (rule6 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is not cold.
("Anne" "is" "cold" "-")
int2
Anne is not furry.
False
4
inv-proof
[(((triple1 ((triple1) -> rule4)) -> rule6))]
("Anne" "is" "furry" "-")
((triple1 ((triple1) -> (rule4 % int2))) -> (rule6 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is not cold.
("Anne" "is" "cold" "-")
int2
Charlie is not quiet.
Unknown
inv-rconc
[@1: Charlie is quiet.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "quiet" "-")
Charlie is furry.
Unknown
rconc
[@1: Charlie is furry.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Charlie" "is" "furry" "+")
Bob is not quiet.
Unknown
inv-rconc
[@1: Bob is quiet.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "quiet" "-")
Charlie is round.
Unknown
random
[@0: Charlie is round.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "round" "+")
Charlie is not big.
Unknown
inv-random
[@0: Charlie is big.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "big" "-")
Bob is green.
Unknown
random
[@0: Bob is green.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "green" "+")
@0: Anne is big.[(triple1)] Anne is green.[(triple2)] Anne is not round.[(triple4)] Anne is quiet.[(triple3)] Bob is cold.[(triple5)] Bob is round.[(triple6)] Charlie is not cold.[(triple7)] @1: Anne is not cold.[(((triple1) -> rule4))] Bob is furry.[(((triple6) -> rule5))] @2: Anne is furry.[(((triple1 ((triple1) -> rule4)) -> rule6))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is green.
("Anne" "is" "green" "+")
triple2
Anne is not round.
("Anne" "is" "round" "-")
triple4
Anne is quiet.
("Anne" "is" "quiet" "+")
triple3
Bob is cold.
("Bob" "is" "cold" "+")
triple5
Bob is round.
("Bob" "is" "round" "+")
triple6
Charlie is not cold.
("Charlie" "is" "cold" "-")
triple7
Anne is not cold.
("Anne" "is" "cold" "-")
((triple1) -> (rule4 % int1))
Anne is not cold.
("Anne" "is" "cold" "-")
int1
Bob is furry.
("Bob" "is" "furry" "+")
((triple6) -> (rule5 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
((triple1 ((triple1) -> (rule4 % int2))) -> (rule6 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is not cold.
("Anne" "is" "cold" "-")
int2