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