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