Anne is round. Bob is white. Dave is round. If Anne is white then Anne is round. If Anne is blue and Anne is furry then Anne is round. If someone is big then they are quiet. If someone is furry and quiet then they are big. Round, white people are cold. If Anne is round then Anne is big.
Anne is round.
("Anne" "is" "round" "+")
Bob is white.
("Bob" "is" "white" "+")
Dave is round.
("Dave" "is" "round" "+")
If Anne is white then Anne is round.
((("Anne" "is" "white" "+")) -> ("Anne" "is" "round" "+"))
If Anne is blue and Anne is furry then Anne is round.
((("Anne" "is" "blue" "+") ("Anne" "is" "furry" "+")) -> ("Anne" "is" "round" "+"))
If someone is big then they are quiet.
((("someone" "is" "big" "+")) -> ("someone" "is" "quiet" "+"))
If someone is furry and quiet then they are big.
((("someone" "is" "furry" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "big" "+"))
Round, white people are cold.
((("someone" "is" "round" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "cold" "+"))
If Anne is round then Anne is big.
((("Anne" "is" "round" "+")) -> ("Anne" "is" "big" "+"))
Dave is round.
True
1
proof
[(triple3)]
("Dave" "is" "round" "+")
triple3
Bob is not white.
False
1
inv-proof
[(triple2)]
("Bob" "is" "white" "-")
triple2
Anne is big.
True
2
proof
[(((triple1) -> rule6))]
("Anne" "is" "big" "+")
((triple1) -> (rule6 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is not big.
False
2
inv-proof
[(((triple1) -> rule6))]
("Anne" "is" "big" "-")
((triple1) -> (rule6 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is quiet.
True
3
proof
[(((((triple1) -> rule6)) -> rule3))]
("Anne" "is" "quiet" "+")
((((triple1) -> (rule6 % int2))) -> (rule3 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is not quiet.
False
3
inv-proof
[(((((triple1) -> rule6)) -> rule3))]
("Anne" "is" "quiet" "-")
((((triple1) -> (rule6 % int2))) -> (rule3 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Dave is not big.
Unknown
inv-rconc
[@1: Dave is big.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Dave" "is" "big" "-")
Bob is quiet.
Unknown
rconc
[@2: Bob is quiet.[CWA. Example of deepest failure = (rule3 <- rule4 <- FAIL)]]
("Bob" "is" "quiet" "+")
Dave is not quiet.
Unknown
inv-rconc
[@2: Dave is quiet.[CWA. Example of deepest failure = (rule3 <- rule4 <- FAIL)]]
("Dave" "is" "quiet" "-")
Dave is white.
Unknown
random
[@0: Dave is white.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "white" "+")
Bob is not blue.
Unknown
inv-random
[@0: Bob is blue.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "blue" "-")
Dave is furry.
Unknown
random
[@0: Dave is furry.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "furry" "+")
@0: Anne is round.[(triple1)] Bob is white.[(triple2)] Dave is round.[(triple3)] @1: Anne is big.[(((triple1) -> rule6))] @2: Anne is quiet.[(((((triple1) -> rule6)) -> rule3))]
Anne is round.
("Anne" "is" "round" "+")
triple1
Bob is white.
("Bob" "is" "white" "+")
triple2
Dave is round.
("Dave" "is" "round" "+")
triple3
Anne is big.
("Anne" "is" "big" "+")
((triple1) -> (rule6 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
((((triple1) -> (rule6 % int2))) -> (rule3 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2