Anne is blue. Anne is nice. Anne is quiet. Anne is round. Bob is big. Bob is green. Bob is nice. Bob is quiet. Charlie is big. Charlie is blue. Charlie is green. Charlie is nice. If something is blue and nice then it is cold. If something is green then it is blue. If something is cold then it is nice.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is round.
("Anne" "is" "round" "+")
Bob is big.
("Bob" "is" "big" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
If something is blue and nice then it is cold.
((("something" "is" "blue" "+") ("something" "is" "nice" "+")) -> ("something" "is" "cold" "+"))
If something is green then it is blue.
((("something" "is" "green" "+")) -> ("something" "is" "blue" "+"))
If something is cold then it is nice.
((("something" "is" "cold" "+")) -> ("something" "is" "nice" "+"))
Bob is quiet.
True
1
proof
[(triple8)]
("Bob" "is" "quiet" "+")
triple8
Charlie is not blue.
False
1
inv-proof
[(triple10 OR ((triple11) -> rule2))]
("Charlie" "is" "blue" "-")
triple10
((triple11) -> (rule2 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Bob is blue.
True
2
proof
[(((triple6) -> rule2))]
("Bob" "is" "blue" "+")
((triple6) -> (rule2 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is not blue.
False
2
inv-proof
[(((triple6) -> rule2))]
("Bob" "is" "blue" "-")
((triple6) -> (rule2 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is cold.
True
4
proof
[(((((triple6) -> rule2) triple7) -> rule1))]
("Bob" "is" "cold" "+")
((((triple6) -> (rule2 % int2)) triple7) -> (rule1 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is not cold.
False
4
inv-proof
[(((((triple6) -> rule2) triple7) -> rule1))]
("Bob" "is" "cold" "-")
((((triple6) -> (rule2 % int2)) triple7) -> (rule1 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Charlie is not quiet.
Unknown
inv-random
[@0: Charlie is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "quiet" "-")
Bob is round.
Unknown
random
[@0: Bob is round.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "round" "+")
Charlie is not round.
Unknown
inv-random
[@0: Charlie is round.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "round" "-")
Anne is green.
Unknown
random
[@0: Anne is green.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "green" "+")
@0: Anne is blue.[(triple1)] Anne is nice.[(triple2)] Anne is quiet.[(triple3)] Anne is round.[(triple4)] Bob is big.[(triple5)] Bob is green.[(triple6)] Bob is nice.[(triple7)] Bob is quiet.[(triple8)] Charlie is big.[(triple9)] Charlie is blue.[(triple10 OR ((triple11) -> rule2))] Charlie is green.[(triple11)] Charlie is nice.[(triple12)] @1: Anne is cold.[(((triple1 triple2) -> rule1))] Bob is blue.[(((triple6) -> rule2))] Charlie is cold.[(((triple10 triple12) -> rule1) OR ((((triple11) -> rule2) triple12) -> rule1))] @2: Bob is cold.[(((((triple6) -> rule2) triple7) -> rule1))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is nice.
("Anne" "is" "nice" "+")
triple2
Anne is quiet.
("Anne" "is" "quiet" "+")
triple3
Anne is round.
("Anne" "is" "round" "+")
triple4
Bob is big.
("Bob" "is" "big" "+")
triple5
Bob is green.
("Bob" "is" "green" "+")
triple6
Bob is nice.
("Bob" "is" "nice" "+")
triple7
Bob is quiet.
("Bob" "is" "quiet" "+")
triple8
Charlie is big.
("Charlie" "is" "big" "+")
triple9
Charlie is blue.
("Charlie" "is" "blue" "+")
triple10
((triple11) -> (rule2 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
triple11
Charlie is nice.
("Charlie" "is" "nice" "+")
triple12
Anne is cold.
("Anne" "is" "cold" "+")
((triple1 triple2) -> (rule1 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
((triple6) -> (rule2 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
((triple10 triple12) -> (rule1 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
((((triple11) -> (rule2 % int2)) triple12) -> (rule1 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
((((triple6) -> (rule2 % int2)) triple7) -> (rule1 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2