Anne is blue. Anne is cold. Anne is furry. Anne is nice. Anne is red. Anne is round. Anne is smart. Dave is cold. Dave is nice. Dave is round. Nice people are furry. All furry people are smart.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is cold.
("Anne" "is" "cold" "+")
Anne is furry.
("Anne" "is" "furry" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is round.
("Anne" "is" "round" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is round.
("Dave" "is" "round" "+")
Nice people are furry.
((("someone" "is" "nice" "+")) -> ("someone" "is" "furry" "+"))
All furry people are smart.
((("someone" "is" "furry" "+")) -> ("someone" "is" "smart" "+"))
Dave is round.
True
1
proof
[(triple10)]
("Dave" "is" "round" "+")
triple10
Dave is not nice.
False
1
inv-proof
[(triple9)]
("Dave" "is" "nice" "-")
triple9
Dave is furry.
True
2
proof
[(((triple9) -> rule1))]
("Dave" "is" "furry" "+")
((triple9) -> (rule1 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is not furry.
False
2
inv-proof
[(((triple9) -> rule1))]
("Dave" "is" "furry" "-")
((triple9) -> (rule1 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is smart.
True
3
proof
[(((((triple9) -> rule1)) -> rule2))]
("Dave" "is" "smart" "+")
((((triple9) -> (rule1 % int2))) -> (rule2 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is not smart.
False
3
inv-proof
[(((((triple9) -> rule1)) -> rule2))]
("Dave" "is" "smart" "-")
((((triple9) -> (rule1 % int2))) -> (rule2 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is not red.
Unknown
inv-random
[@0: Dave is red.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "red" "-")
Dave is blue.
Unknown
random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "+")
@0: Anne is blue.[(triple1)] Anne is cold.[(triple2)] Anne is furry.[(triple3 OR ((triple4) -> rule1))] Anne is nice.[(triple4)] Anne is red.[(triple5)] Anne is round.[(triple6)] Anne is smart.[(triple7 OR ((triple3) -> rule2) OR ((((triple4) -> rule1)) -> rule2))] Dave is cold.[(triple8)] Dave is nice.[(triple9)] Dave is round.[(triple10)] @1: Dave is furry.[(((triple9) -> rule1))] @2: Dave is smart.[(((((triple9) -> rule1)) -> rule2))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is cold.
("Anne" "is" "cold" "+")
triple2
Anne is furry.
("Anne" "is" "furry" "+")
triple3
((triple4) -> (rule1 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
triple4
Anne is red.
("Anne" "is" "red" "+")
triple5
Anne is round.
("Anne" "is" "round" "+")
triple6
Anne is smart.
("Anne" "is" "smart" "+")
triple7
((triple3) -> (rule2 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
((((triple4) -> (rule1 % int2))) -> (rule2 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
triple8
Dave is nice.
("Dave" "is" "nice" "+")
triple9
Dave is round.
("Dave" "is" "round" "+")
triple10
Dave is furry.
("Dave" "is" "furry" "+")
((triple9) -> (rule1 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
((((triple9) -> (rule1 % int2))) -> (rule2 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2