Anne is blue. Anne is cold. Anne is furry. Bob is round. Bob is white. Charlie is cold. Charlie is furry. Charlie is green. Charlie is red. Gary is furry. All green people are blue. If Gary is green then Gary is cold. If Bob is white then Bob is cold. If someone is white then they are green. If Gary is furry then Gary is white. Red people are blue.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is cold.
("Anne" "is" "cold" "+")
Anne is furry.
("Anne" "is" "furry" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is white.
("Bob" "is" "white" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Gary is furry.
("Gary" "is" "furry" "+")
All green people are blue.
((("someone" "is" "green" "+")) -> ("someone" "is" "blue" "+"))
If Gary is green then Gary is cold.
((("Gary" "is" "green" "+")) -> ("Gary" "is" "cold" "+"))
If Bob is white then Bob is cold.
((("Bob" "is" "white" "+")) -> ("Bob" "is" "cold" "+"))
If someone is white then they are green.
((("someone" "is" "white" "+")) -> ("someone" "is" "green" "+"))
If Gary is furry then Gary is white.
((("Gary" "is" "furry" "+")) -> ("Gary" "is" "white" "+"))
Red people are blue.
((("someone" "is" "red" "+")) -> ("someone" "is" "blue" "+"))
Charlie is green.
True
1
proof
[(triple8)]
("Charlie" "is" "green" "+")
triple8
Bob is not round.
False
1
inv-proof
[(triple4)]
("Bob" "is" "round" "-")
triple4
Charlie is blue.
True
2
proof
[(((triple8) -> rule1) OR ((triple9) -> rule6))]
("Charlie" "is" "blue" "+")
((triple8) -> (rule1 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
((triple9) -> (rule6 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Bob is not green.
False
2
inv-proof
[(((triple5) -> rule4))]
("Bob" "is" "green" "-")
((triple5) -> (rule4 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Gary is green.
True
3
proof
[(((((triple10) -> rule5)) -> rule4))]
("Gary" "is" "green" "+")
((((triple10) -> (rule5 % int2))) -> (rule4 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is not green.
False
3
inv-proof
[(((((triple10) -> rule5)) -> rule4))]
("Gary" "is" "green" "-")
((((triple10) -> (rule5 % int2))) -> (rule4 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is cold.
True
4
proof
[(((((((triple10) -> rule5)) -> rule4)) -> rule2))]
("Gary" "is" "cold" "+")
((((((triple10) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
Gary is not blue.
False
4
inv-proof
[(((((((triple10) -> rule5)) -> rule4)) -> rule1))]
("Gary" "is" "blue" "-")
((((((triple10) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
Anne is not green.
Unknown
inv-rconc
[@1: Anne is green.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Anne" "is" "green" "-")
Bob is furry.
Unknown
random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "+")
Gary is not round.
Unknown
inv-random
[@0: Gary is round.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "round" "-")
Gary is red.
Unknown
random
[@0: Gary is red.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "red" "+")
Charlie is not white.
Unknown
inv-random
[@0: Charlie is white.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "white" "-")
Anne is round.
Unknown
random
[@0: Anne is round.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "round" "+")
Anne is not white.
Unknown
inv-random
[@0: Anne is white.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "white" "-")
Bob is red.
Unknown
random
[@0: Bob is red.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "red" "+")
@0: Anne is blue.[(triple1)] Anne is cold.[(triple2)] Anne is furry.[(triple3)] Bob is round.[(triple4)] Bob is white.[(triple5)] Charlie is cold.[(triple6)] Charlie is furry.[(triple7)] Charlie is green.[(triple8)] Charlie is red.[(triple9)] Gary is furry.[(triple10)] @1: Bob is cold.[(((triple5) -> rule3))] Bob is green.[(((triple5) -> rule4))] Charlie is blue.[(((triple8) -> rule1) OR ((triple9) -> rule6))] Gary is white.[(((triple10) -> rule5))] @2: Bob is blue.[(((((triple5) -> rule4)) -> rule1))] Gary is green.[(((((triple10) -> rule5)) -> rule4))] @3: Gary is blue.[(((((((triple10) -> rule5)) -> rule4)) -> rule1))] Gary is cold.[(((((((triple10) -> rule5)) -> rule4)) -> rule2))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is cold.
("Anne" "is" "cold" "+")
triple2
Anne is furry.
("Anne" "is" "furry" "+")
triple3
Bob is round.
("Bob" "is" "round" "+")
triple4
Bob is white.
("Bob" "is" "white" "+")
triple5
Charlie is cold.
("Charlie" "is" "cold" "+")
triple6
Charlie is furry.
("Charlie" "is" "furry" "+")
triple7
Charlie is green.
("Charlie" "is" "green" "+")
triple8
Charlie is red.
("Charlie" "is" "red" "+")
triple9
Gary is furry.
("Gary" "is" "furry" "+")
triple10
Bob is cold.
("Bob" "is" "cold" "+")
((triple5) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
((triple5) -> (rule4 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
((triple8) -> (rule1 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
((triple9) -> (rule6 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
((triple10) -> (rule5 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
((((triple5) -> (rule4 % int2))) -> (rule1 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
((((triple10) -> (rule5 % int2))) -> (rule4 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
((((((triple10) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
Gary is cold.
("Gary" "is" "cold" "+")
((((((triple10) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3