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