Anne is furry. Anne is quiet. Anne is round. Bob is quiet. Bob is red. Bob is round. Harry is furry. Harry is quiet. Harry is round. Harry is white. If something is red then it is blue. All blue, red things are cold. Round things are red.
Anne is furry.
("Anne" "is" "furry" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is round.
("Anne" "is" "round" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is round.
("Bob" "is" "round" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is white.
("Harry" "is" "white" "+")
If something is red then it is blue.
((("something" "is" "red" "+")) -> ("something" "is" "blue" "+"))
All blue, red things are cold.
((("something" "is" "blue" "+") ("something" "is" "red" "+")) -> ("something" "is" "cold" "+"))
Round things are red.
((("something" "is" "round" "+")) -> ("something" "is" "red" "+"))
Anne is furry.
True
1
proof
[(triple1)]
("Anne" "is" "furry" "+")
triple1
Anne is not quiet.
False
1
inv-proof
[(triple2)]
("Anne" "is" "quiet" "-")
triple2
Anne is red.
True
2
proof
[(((triple3) -> rule3))]
("Anne" "is" "red" "+")
((triple3) -> (rule3 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Harry is not red.
False
2
inv-proof
[(((triple9) -> rule3))]
("Harry" "is" "red" "-")
((triple9) -> (rule3 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is blue.
True
3
proof
[(((((triple9) -> rule3)) -> rule1))]
("Harry" "is" "blue" "+")
((((triple9) -> (rule3 % int2))) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is not blue.
False
3
inv-proof
[(((((triple9) -> rule3)) -> rule1))]
("Harry" "is" "blue" "-")
((((triple9) -> (rule3 % int2))) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Anne is cold.
True
6
proof
[(((((((triple3) -> rule3)) -> rule1) ((triple3) -> rule3)) -> rule2))]
("Anne" "is" "cold" "+")
((((((triple3) -> (rule3 % int3))) -> (rule1 % int2)) ((triple3) -> (rule3 % int3))) -> (rule2 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3
Harry is not cold.
False
6
inv-proof
[(((((((triple9) -> rule3)) -> rule1) ((triple9) -> rule3)) -> rule2))]
("Harry" "is" "cold" "-")
((((((triple9) -> (rule3 % int3))) -> (rule1 % int2)) ((triple9) -> (rule3 % int3))) -> (rule2 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
int3
Bob is not furry.
Unknown
inv-random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "-")
Bob is white.
Unknown
random
[@0: Bob is white.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "white" "+")
@0: Anne is furry.[(triple1)] Anne is quiet.[(triple2)] Anne is round.[(triple3)] Bob is quiet.[(triple4)] Bob is red.[(triple5 OR ((triple6) -> rule3))] Bob is round.[(triple6)] Harry is furry.[(triple7)] Harry is quiet.[(triple8)] Harry is round.[(triple9)] Harry is white.[(triple10)] @1: Anne is red.[(((triple3) -> rule3))] Bob is blue.[(((triple5) -> rule1) OR ((((triple6) -> rule3)) -> rule1))] Harry is red.[(((triple9) -> rule3))] @2: Anne is blue.[(((((triple3) -> rule3)) -> rule1))] Bob is cold.[(((((triple5) -> rule1) triple5) -> rule2) OR ((((triple5) -> rule1) ((triple6) -> rule3)) -> rule2) OR ((((((triple6) -> rule3)) -> rule1) triple5) -> rule2) OR ((((((triple6) -> rule3)) -> rule1) ((triple6) -> rule3)) -> rule2))] Harry is blue.[(((((triple9) -> rule3)) -> rule1))] @3: Anne is cold.[(((((((triple3) -> rule3)) -> rule1) ((triple3) -> rule3)) -> rule2))] Harry is cold.[(((((((triple9) -> rule3)) -> rule1) ((triple9) -> rule3)) -> rule2))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
Anne is quiet.
("Anne" "is" "quiet" "+")
triple2
Anne is round.
("Anne" "is" "round" "+")
triple3
Bob is quiet.
("Bob" "is" "quiet" "+")
triple4
Bob is red.
("Bob" "is" "red" "+")
triple5
((triple6) -> (rule3 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
triple6
Harry is furry.
("Harry" "is" "furry" "+")
triple7
Harry is quiet.
("Harry" "is" "quiet" "+")
triple8
Harry is round.
("Harry" "is" "round" "+")
triple9
Harry is white.
("Harry" "is" "white" "+")
triple10
Anne is red.
("Anne" "is" "red" "+")
((triple3) -> (rule3 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
((triple5) -> (rule1 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
((((triple6) -> (rule3 % int2))) -> (rule1 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
((triple9) -> (rule3 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
((((triple3) -> (rule3 % int2))) -> (rule1 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
((((triple5) -> (rule1 % int2)) triple5) -> (rule2 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
((((triple5) -> (rule1 % int3)) ((triple6) -> (rule3 % int2))) -> (rule2 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
((((((triple6) -> (rule3 % int3))) -> (rule1 % int2)) triple5) -> (rule2 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
((((((triple6) -> (rule3 % int3))) -> (rule1 % int2)) ((triple6) -> (rule3 % int3))) -> (rule2 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
Harry is blue.
("Harry" "is" "blue" "+")
((((triple9) -> (rule3 % int2))) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
((((((triple3) -> (rule3 % int3))) -> (rule1 % int2)) ((triple3) -> (rule3 % int3))) -> (rule2 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3
Harry is cold.
("Harry" "is" "cold" "+")
((((((triple9) -> (rule3 % int3))) -> (rule1 % int2)) ((triple9) -> (rule3 % int3))) -> (rule2 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
int3