Anne is round. Erin is kind. Erin is white. Fiona is cold. Fiona is green. Fiona is kind. Fiona is round. Fiona is white. Gary is cold. Gary is green. Gary is kind. Gary is rough. Kind people are green. If someone is rough and cold then they are round. Nice, green people are cold. White people are kind. All kind, green people are cold. All rough, kind people are round.
Anne is round.
("Anne" "is" "round" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is white.
("Erin" "is" "white" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
Fiona is round.
("Fiona" "is" "round" "+")
Fiona is white.
("Fiona" "is" "white" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Kind people are green.
((("someone" "is" "kind" "+")) -> ("someone" "is" "green" "+"))
If someone is rough and cold then they are round.
((("someone" "is" "rough" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "round" "+"))
Nice, green people are cold.
((("someone" "is" "nice" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "cold" "+"))
White people are kind.
((("someone" "is" "white" "+")) -> ("someone" "is" "kind" "+"))
All kind, green people are cold.
((("someone" "is" "kind" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "cold" "+"))
All rough, kind people are round.
((("someone" "is" "rough" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "round" "+"))
Erin is white.
True
1
proof
[(triple3)]
("Erin" "is" "white" "+")
triple3
Fiona is not kind.
False
1
inv-proof
[(triple6 OR ((triple8) -> rule4))]
("Fiona" "is" "kind" "-")
triple6
((triple8) -> (rule4 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Gary is round.
True
3
proof
[(((triple12 triple11) -> rule6) OR ((triple12 triple9) -> rule2) OR ((triple12 ((triple11 triple10) -> rule5)) -> rule2) OR ((triple12 ((triple11 ((triple11) -> rule1)) -> rule5)) -> rule2))]
("Gary" "is" "round" "+")
((triple12 triple11) -> (rule6 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
((triple12 triple9) -> (rule2 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
((triple12 ((triple11 triple10) -> (rule5 % int2))) -> (rule2 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
((triple12 ((triple11 ((triple11) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3
Gary is not round.
False
3
inv-proof
[(((triple12 triple11) -> rule6) OR ((triple12 triple9) -> rule2) OR ((triple12 ((triple11 triple10) -> rule5)) -> rule2) OR ((triple12 ((triple11 ((triple11) -> rule1)) -> rule5)) -> rule2))]
("Gary" "is" "round" "-")
((triple12 triple11) -> (rule6 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
((triple12 triple9) -> (rule2 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
((triple12 ((triple11 triple10) -> (rule5 % int2))) -> (rule2 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
((triple12 ((triple11 ((triple11) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3
Erin is cold.
True
4
proof
[(((triple2 ((triple2) -> rule1)) -> rule5) OR ((((triple3) -> rule4) ((triple2) -> rule1)) -> rule5) OR ((triple2 ((((triple3) -> rule4)) -> rule1)) -> rule5) OR ((((triple3) -> rule4) ((((triple3) -> rule4)) -> rule1)) -> rule5))]
("Erin" "is" "cold" "+")
((triple2 ((triple2) -> (rule1 % int2))) -> (rule5 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
((((triple3) -> (rule4 % int3)) ((triple2) -> (rule1 % int2))) -> (rule5 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
((triple2 ((((triple3) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
((((triple3) -> (rule4 % int3)) ((((triple3) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Erin is not cold.
False
4
inv-proof
[(((triple2 ((triple2) -> rule1)) -> rule5) OR ((((triple3) -> rule4) ((triple2) -> rule1)) -> rule5) OR ((triple2 ((((triple3) -> rule4)) -> rule1)) -> rule5) OR ((((triple3) -> rule4) ((((triple3) -> rule4)) -> rule1)) -> rule5))]
("Erin" "is" "cold" "-")
((triple2 ((triple2) -> (rule1 % int2))) -> (rule5 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
((((triple3) -> (rule4 % int3)) ((triple2) -> (rule1 % int2))) -> (rule5 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
((triple2 ((((triple3) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
((((triple3) -> (rule4 % int3)) ((((triple3) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Erin is not round.
Unknown
inv-rconc
[@1: Erin is round.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Erin" "is" "round" "-")
Anne is cold.
Unknown
rconc
[@2: Anne is cold.[CWA. Example of deepest failure = (rule5 <- rule4 <- FAIL)]]
("Anne" "is" "cold" "+")
Anne is not kind.
Unknown
inv-rconc
[@1: Anne is kind.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Anne" "is" "kind" "-")
Anne is rough.
Unknown
random
[@0: Anne is rough.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "rough" "+")
Anne is not white.
Unknown
inv-random
[@0: Anne is white.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "white" "-")
Fiona is nice.
Unknown
random
[@0: Fiona is nice.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "nice" "+")
@0: Anne is round.[(triple1)] Erin is kind.[(triple2 OR ((triple3) -> rule4))] Erin is white.[(triple3)] Fiona is cold.[(triple4 OR ((triple6 triple5) -> rule5) OR ((triple6 ((triple6) -> rule1)) -> rule5) OR ((((triple8) -> rule4) triple5) -> rule5) OR ((((triple8) -> rule4) ((triple6) -> rule1)) -> rule5) OR ((triple6 ((((triple8) -> rule4)) -> rule1)) -> rule5) OR ((((triple8) -> rule4) ((((triple8) -> rule4)) -> rule1)) -> rule5))] Fiona is green.[(triple5 OR ((triple6) -> rule1) OR ((((triple8) -> rule4)) -> rule1))] Fiona is kind.[(triple6 OR ((triple8) -> rule4))] Fiona is round.[(triple7)] Fiona is white.[(triple8)] Gary is cold.[(triple9 OR ((triple11 triple10) -> rule5) OR ((triple11 ((triple11) -> rule1)) -> rule5))] Gary is green.[(triple10 OR ((triple11) -> rule1))] Gary is kind.[(triple11)] Gary is rough.[(triple12)] @1: Erin is green.[(((triple2) -> rule1) OR ((((triple3) -> rule4)) -> rule1))] Gary is round.[(((triple12 triple11) -> rule6) OR ((triple12 triple9) -> rule2) OR ((triple12 ((triple11 triple10) -> rule5)) -> rule2) OR ((triple12 ((triple11 ((triple11) -> rule1)) -> rule5)) -> rule2))] @2: Erin is cold.[(((triple2 ((triple2) -> rule1)) -> rule5) OR ((((triple3) -> rule4) ((triple2) -> rule1)) -> rule5) OR ((triple2 ((((triple3) -> rule4)) -> rule1)) -> rule5) OR ((((triple3) -> rule4) ((((triple3) -> rule4)) -> rule1)) -> rule5))]
Anne is round.
("Anne" "is" "round" "+")
triple1
Erin is kind.
("Erin" "is" "kind" "+")
triple2
((triple3) -> (rule4 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
triple3
Fiona is cold.
("Fiona" "is" "cold" "+")
triple4
((triple6 triple5) -> (rule5 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
((triple6 ((triple6) -> (rule1 % int2))) -> (rule5 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
((((triple8) -> (rule4 % int2)) triple5) -> (rule5 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
((((triple8) -> (rule4 % int3)) ((triple6) -> (rule1 % int2))) -> (rule5 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
int3
((triple6 ((((triple8) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
int3
((((triple8) -> (rule4 % int3)) ((((triple8) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
int3
Fiona is green.
("Fiona" "is" "green" "+")
triple5
((triple6) -> (rule1 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
((((triple8) -> (rule4 % int2))) -> (rule1 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
triple6
((triple8) -> (rule4 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
triple7
Fiona is white.
("Fiona" "is" "white" "+")
triple8
Gary is cold.
("Gary" "is" "cold" "+")
triple9
((triple11 triple10) -> (rule5 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
((triple11 ((triple11) -> (rule1 % int2))) -> (rule5 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
triple10
((triple11) -> (rule1 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
triple11
Gary is rough.
("Gary" "is" "rough" "+")
triple12
Erin is green.
("Erin" "is" "green" "+")
((triple2) -> (rule1 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
((((triple3) -> (rule4 % int2))) -> (rule1 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
((triple12 triple11) -> (rule6 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
((triple12 triple9) -> (rule2 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
((triple12 ((triple11 triple10) -> (rule5 % int2))) -> (rule2 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
((triple12 ((triple11 ((triple11) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3
Erin is cold.
("Erin" "is" "cold" "+")
((triple2 ((triple2) -> (rule1 % int2))) -> (rule5 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
((((triple3) -> (rule4 % int3)) ((triple2) -> (rule1 % int2))) -> (rule5 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
((triple2 ((((triple3) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
((((triple3) -> (rule4 % int3)) ((((triple3) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3