Anne is green. Anne is round. Anne is not smart. Anne is white. Bob is green. Bob is quiet. Bob is round. Gary is cold. Gary is smart. Gary is not white. If something is cold and not round then it is green. If something is cold then it is green. Cold things are green. All smart things are red. If something is green then it is red. If Gary is round and Gary is quiet then Gary is not smart. If Gary is round and Gary is smart then Gary is white. All red things are quiet.
Anne is green.
("Anne" "is" "green" "+")
Anne is round.
("Anne" "is" "round" "+")
Anne is not smart.
("Anne" "is" "smart" "-")
Anne is white.
("Anne" "is" "white" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is round.
("Bob" "is" "round" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Gary is not white.
("Gary" "is" "white" "-")
If something is cold and not round then it is green.
((("something" "is" "cold" "+") ("something" "is" "round" "~")) -> ("something" "is" "green" "+"))
If something is cold then it is green.
((("something" "is" "cold" "+")) -> ("something" "is" "green" "+"))
Cold things are green.
((("something" "is" "cold" "+")) -> ("something" "is" "green" "+"))
All smart things are red.
((("something" "is" "smart" "+")) -> ("something" "is" "red" "+"))
If something is green then it is red.
((("something" "is" "green" "+")) -> ("something" "is" "red" "+"))
If Gary is round and Gary is quiet then Gary is not smart.
((("Gary" "is" "round" "+") ("Gary" "is" "quiet" "+")) -> ("Gary" "is" "smart" "-"))
If Gary is round and Gary is smart then Gary is white.
((("Gary" "is" "round" "+") ("Gary" "is" "smart" "+")) -> ("Gary" "is" "white" "+"))
All red things are quiet.
((("something" "is" "red" "+")) -> ("something" "is" "quiet" "+"))
Gary is cold.
True
1
proof
[(triple8)]
("Gary" "is" "cold" "+")
triple8
Anne is smart.
False
1
inv-proof
[(triple3)]
("Anne" "is" "smart" "+")
triple3
Anne is red.
True
2
proof
[(((triple1) -> rule5))]
("Anne" "is" "red" "+")
((triple1) -> (rule5 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Bob is not red.
False
2
inv-proof
[(((triple5) -> rule5))]
("Bob" "is" "red" "-")
((triple5) -> (rule5 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Gary is quiet.
True
3
proof
[(((((triple9) -> rule4)) -> rule8) OR ((((((triple8) -> rule2)) -> rule5)) -> rule8) OR ((((((triple8) -> rule3)) -> rule5)) -> rule8))]
("Gary" "is" "quiet" "+")
((((triple9) -> (rule4 % int2))) -> (rule8 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
((((((triple8) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3
((((((triple8) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3
Gary is not quiet.
False
3
inv-proof
[(((((triple9) -> rule4)) -> rule8) OR ((((((triple8) -> rule2)) -> rule5)) -> rule8) OR ((((((triple8) -> rule3)) -> rule5)) -> rule8))]
("Gary" "is" "quiet" "-")
((((triple9) -> (rule4 % int2))) -> (rule8 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
((((((triple8) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3
((((((triple8) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3
Bob is not smart.
Unknown
inv-random
[@0: Bob is smart.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "smart" "-")
Bob is cold.
Unknown
random
[@0: Bob is cold.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "cold" "+")
Anne is not cold.
Unknown
inv-random
[@0: Anne is cold.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "cold" "-")
Bob is white.
Unknown
random
[@0: Bob is white.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "white" "+")
@0: Anne is green.[(triple1)] Anne is not smart.[(triple3)] Anne is round.[(triple2)] Anne is white.[(triple4)] Bob is green.[(triple5)] Bob is quiet.[(triple6 OR ((((triple5) -> rule5)) -> rule8))] Bob is round.[(triple7)] Gary is cold.[(triple8)] Gary is not white.[(triple10)] Gary is smart.[(triple9)] @1: Anne is red.[(((triple1) -> rule5))] Bob is red.[(((triple5) -> rule5))] Gary is green.[(((triple8) -> rule2) OR ((triple8) -> rule3))] Gary is red.[(((triple9) -> rule4) OR ((((triple8) -> rule2)) -> rule5) OR ((((triple8) -> rule3)) -> rule5))] @2: Anne is quiet.[(((((triple1) -> rule5)) -> rule8))] Gary is quiet.[(((((triple9) -> rule4)) -> rule8) OR ((((((triple8) -> rule2)) -> rule5)) -> rule8) OR ((((((triple8) -> rule3)) -> rule5)) -> rule8))]
Anne is green.
("Anne" "is" "green" "+")
triple1
Anne is not smart.
("Anne" "is" "smart" "-")
triple3
Anne is round.
("Anne" "is" "round" "+")
triple2
Anne is white.
("Anne" "is" "white" "+")
triple4
Bob is green.
("Bob" "is" "green" "+")
triple5
Bob is quiet.
("Bob" "is" "quiet" "+")
triple6
((((triple5) -> (rule5 % int2))) -> (rule8 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
triple7
Gary is cold.
("Gary" "is" "cold" "+")
triple8
Gary is not white.
("Gary" "is" "white" "-")
triple10
Gary is smart.
("Gary" "is" "smart" "+")
triple9
Anne is red.
("Anne" "is" "red" "+")
((triple1) -> (rule5 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
((triple5) -> (rule5 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
((triple8) -> (rule2 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
((triple8) -> (rule3 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
((triple9) -> (rule4 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
((((triple8) -> (rule2 % int2))) -> (rule5 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
((((triple8) -> (rule3 % int2))) -> (rule5 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
((((triple1) -> (rule5 % int2))) -> (rule8 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
((((triple9) -> (rule4 % int2))) -> (rule8 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
((((((triple8) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3
((((((triple8) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3