Anne is quiet. Dave is not quiet. If something is furry then it is white. Quiet things are cold. Quiet, smart things are young. All cold things are young. If something is cold then it is round. If Anne is not white then Anne is cold. If Anne is round then Anne is young. If Dave is white and Dave is not round then Dave is not young.
Anne is quiet.
("Anne" "is" "quiet" "+")
Dave is not quiet.
("Dave" "is" "quiet" "-")
If something is furry then it is white.
((("something" "is" "furry" "+")) -> ("something" "is" "white" "+"))
Quiet things are cold.
((("something" "is" "quiet" "+")) -> ("something" "is" "cold" "+"))
Quiet, smart things are young.
((("something" "is" "quiet" "+") ("something" "is" "smart" "+")) -> ("something" "is" "young" "+"))
All cold things are young.
((("something" "is" "cold" "+")) -> ("something" "is" "young" "+"))
If something is cold then it is round.
((("something" "is" "cold" "+")) -> ("something" "is" "round" "+"))
If Anne is not white then Anne is cold.
((("Anne" "is" "white" "~")) -> ("Anne" "is" "cold" "+"))
If Anne is round then Anne is young.
((("Anne" "is" "round" "+")) -> ("Anne" "is" "young" "+"))
If Dave is white and Dave is not round then Dave is not young.
((("Dave" "is" "white" "+") ("Dave" "is" "round" "~")) -> ("Dave" "is" "young" "-"))
Anne is quiet.
True
1
proof
[(triple1)]
("Anne" "is" "quiet" "+")
triple1
Anne is not quiet.
False
1
inv-proof
[(triple1)]
("Anne" "is" "quiet" "-")
triple1
Anne is cold.
True
2
proof
[(((triple1) -> rule2))]
("Anne" "is" "cold" "+")
((triple1) -> (rule2 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is not cold.
False
2
inv-proof
[(((triple1) -> rule2))]
("Anne" "is" "cold" "-")
((triple1) -> (rule2 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is young.
True
3
proof
[(((((triple1) -> rule2)) -> rule4) OR ((((((triple1) -> rule2)) -> rule5)) -> rule7))]
("Anne" "is" "young" "+")
((((triple1) -> (rule2 % int2))) -> (rule4 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
((((((triple1) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
Anne is not young.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule4) OR ((((((triple1) -> rule2)) -> rule5)) -> rule7))]
("Anne" "is" "young" "-")
((((triple1) -> (rule2 % int2))) -> (rule4 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
((((((triple1) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
Dave is not young.
Unknown
inv-rconc
[@2: Dave is young.[CWA. Example of deepest failure = (rule4 <- rule2 <- FAIL)]]
("Dave" "is" "young" "-")
Dave is white.
Unknown
rconc
[@1: Dave is white.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "white" "+")
Anne is not white.
Unknown
inv-rconc
[@1: Anne is white.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Anne" "is" "white" "-")
Dave is furry.
Unknown
random
[@0: Dave is furry.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "furry" "+")
Dave is not smart.
Unknown
inv-random
[@0: Dave is smart.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "smart" "-")
Anne is furry.
Unknown
random
[@0: Anne is furry.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "furry" "+")
@0: Anne is quiet.[(triple1)] Dave is not quiet.[(triple2)] @1: Anne is cold.[(((triple1) -> rule2))] @2: Anne is round.[(((((triple1) -> rule2)) -> rule5))] Anne is young.[(((((triple1) -> rule2)) -> rule4) OR ((((((triple1) -> rule2)) -> rule5)) -> rule7))]
Anne is quiet.
("Anne" "is" "quiet" "+")
triple1
Dave is not quiet.
("Dave" "is" "quiet" "-")
triple2
Anne is cold.
("Anne" "is" "cold" "+")
((triple1) -> (rule2 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
((((triple1) -> (rule2 % int2))) -> (rule5 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
((((triple1) -> (rule2 % int2))) -> (rule4 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
((((((triple1) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3