Anne is quiet. Dave is big. Erin is not furry. Rough things are cold. If Anne is young then Anne is big. All big things are young. All furry things are quiet. Young things are furry. If something is big and not young then it is furry.
Anne is quiet.
("Anne" "is" "quiet" "+")
Dave is big.
("Dave" "is" "big" "+")
Erin is not furry.
("Erin" "is" "furry" "-")
Rough things are cold.
((("something" "is" "rough" "+")) -> ("something" "is" "cold" "+"))
If Anne is young then Anne is big.
((("Anne" "is" "young" "+")) -> ("Anne" "is" "big" "+"))
All big things are young.
((("something" "is" "big" "+")) -> ("something" "is" "young" "+"))
All furry things are quiet.
((("something" "is" "furry" "+")) -> ("something" "is" "quiet" "+"))
Young things are furry.
((("something" "is" "young" "+")) -> ("something" "is" "furry" "+"))
If something is big and not young then it is furry.
((("something" "is" "big" "+") ("something" "is" "young" "~")) -> ("something" "is" "furry" "+"))
Dave is big.
True
1
proof
[(triple2)]
("Dave" "is" "big" "+")
triple2
Anne is not quiet.
False
1
inv-proof
[(triple1)]
("Anne" "is" "quiet" "-")
triple1
Dave is young.
True
2
proof
[(((triple2) -> rule3))]
("Dave" "is" "young" "+")
((triple2) -> (rule3 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is not young.
False
2
inv-proof
[(((triple2) -> rule3))]
("Dave" "is" "young" "-")
((triple2) -> (rule3 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is furry.
True
3
proof
[(((((triple2) -> rule3)) -> rule5))]
("Dave" "is" "furry" "+")
((((triple2) -> (rule3 % int2))) -> (rule5 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is not furry.
False
3
inv-proof
[(((((triple2) -> rule3)) -> rule5))]
("Dave" "is" "furry" "-")
((((triple2) -> (rule3 % int2))) -> (rule5 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is quiet.
True
4
proof
[(((((((triple2) -> rule3)) -> rule5)) -> rule4))]
("Dave" "is" "quiet" "+")
((((((triple2) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Dave is not quiet.
False
4
inv-proof
[(((((((triple2) -> rule3)) -> rule5)) -> rule4))]
("Dave" "is" "quiet" "-")
((((((triple2) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Erin is not quiet.
Unknown
inv-rconc
[@1: Erin is quiet.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Erin" "is" "quiet" "-")
Anne is furry.
Unknown
rconc
[@3: Anne is furry.[CWA. Example of deepest failure = (rule5 <- rule3 <- rule2 <- FAIL)]]
("Anne" "is" "furry" "+")
Anne is not big.
Unknown
inv-rconc
[@2: Anne is big.[CWA. Example of deepest failure = (rule2 <- rule3 <- FAIL)]]
("Anne" "is" "big" "-")
Anne is young.
Unknown
rconc
[@2: Anne is young.[CWA. Example of deepest failure = (rule3 <- rule2 <- FAIL)]]
("Anne" "is" "young" "+")
Anne is not round.
Unknown
inv-random
[@0: Anne is round.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "round" "-")
Erin is round.
Unknown
random
[@0: Erin is round.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "round" "+")
Dave is not round.
Unknown
inv-random
[@0: Dave is round.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "round" "-")
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 big.[(triple2)] Erin is not furry.[(triple3)] @1: Dave is young.[(((triple2) -> rule3))] @2: Dave is furry.[(((((triple2) -> rule3)) -> rule5))] @3: Dave is quiet.[(((((((triple2) -> rule3)) -> rule5)) -> rule4))]
Anne is quiet.
("Anne" "is" "quiet" "+")
triple1
Dave is big.
("Dave" "is" "big" "+")
triple2
Erin is not furry.
("Erin" "is" "furry" "-")
triple3
Dave is young.
("Dave" "is" "young" "+")
((triple2) -> (rule3 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
((((triple2) -> (rule3 % int2))) -> (rule5 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
((((((triple2) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3