Anne is furry. Dave is big. If Anne is furry then Anne is round. All round things are big. If Anne is big then Anne is smart.
Anne is furry.
("Anne" "is" "furry" "+")
Dave is big.
("Dave" "is" "big" "+")
If Anne is furry then Anne is round.
((("Anne" "is" "furry" "+")) -> ("Anne" "is" "round" "+"))
All round things are big.
((("something" "is" "round" "+")) -> ("something" "is" "big" "+"))
If Anne is big then Anne is smart.
((("Anne" "is" "big" "+")) -> ("Anne" "is" "smart" "+"))
Anne is furry.
True
1
proof
[(triple1)]
("Anne" "is" "furry" "+")
triple1
Anne is not furry.
False
1
inv-proof
[(triple1)]
("Anne" "is" "furry" "-")
triple1
Anne is round.
True
2
proof
[(((triple1) -> rule1))]
("Anne" "is" "round" "+")
((triple1) -> (rule1 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is not round.
False
2
inv-proof
[(((triple1) -> rule1))]
("Anne" "is" "round" "-")
((triple1) -> (rule1 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is big.
True
3
proof
[(((((triple1) -> rule1)) -> rule2))]
("Anne" "is" "big" "+")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is not big.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule2))]
("Anne" "is" "big" "-")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is smart.
True
4
proof
[(((((((triple1) -> rule1)) -> rule2)) -> rule3))]
("Anne" "is" "smart" "+")
((((((triple1) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
int3
Anne is not smart.
False
4
inv-proof
[(((((((triple1) -> rule1)) -> rule2)) -> rule3))]
("Anne" "is" "smart" "-")
((((((triple1) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
int3
Anne is not blue.
Unknown
inv-random
[@0: Anne is blue.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "blue" "-")
Dave is smart.
Unknown
random
[@0: Dave is smart.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "smart" "+")
Dave is not furry.
Unknown
inv-random
[@0: Dave is furry.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "furry" "-")
Dave is blue.
Unknown
random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "+")
Dave is not cold.
Unknown
inv-random
[@0: Dave is cold.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "cold" "-")
Dave is round.
Unknown
random
[@0: Dave is round.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "round" "+")
Anne is not white.
Unknown
inv-random
[@0: Anne is white.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "white" "-")
Anne is cold.
Unknown
random
[@0: Anne is cold.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "cold" "+")
@0: Anne is furry.[(triple1)] Dave is big.[(triple2)] @1: Anne is round.[(((triple1) -> rule1))] @2: Anne is big.[(((((triple1) -> rule1)) -> rule2))] @3: Anne is smart.[(((((((triple1) -> rule1)) -> rule2)) -> rule3))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
Dave is big.
("Dave" "is" "big" "+")
triple2
Anne is round.
("Anne" "is" "round" "+")
((triple1) -> (rule1 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
((((((triple1) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
int3