Anne is big. Anne is cold. Anne is furry. Anne is rough. Erin is not blue. Erin is furry. Erin is not green. Erin is kind. Erin is rough. Gary is big. Gary is cold. Gary is furry. Gary is green. Gary is kind. Gary is rough. All green things are blue. If Anne is green and Anne is blue then Anne is furry. If Erin is furry and Erin is not green then Erin is not blue. If something is furry and not blue then it is big. All big things are cold. If something is big and furry then it is cold.
Anne is big.
("Anne" "is" "big" "+")
Anne is cold.
("Anne" "is" "cold" "+")
Anne is furry.
("Anne" "is" "furry" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Erin is not blue.
("Erin" "is" "blue" "-")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is not green.
("Erin" "is" "green" "-")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is rough.
("Gary" "is" "rough" "+")
All green things are blue.
((("something" "is" "green" "+")) -> ("something" "is" "blue" "+"))
If Anne is green and Anne is blue then Anne is furry.
((("Anne" "is" "green" "+") ("Anne" "is" "blue" "+")) -> ("Anne" "is" "furry" "+"))
If Erin is furry and Erin is not green then Erin is not blue.
((("Erin" "is" "furry" "+") ("Erin" "is" "green" "~")) -> ("Erin" "is" "blue" "-"))
If something is furry and not blue then it is big.
((("something" "is" "furry" "+") ("something" "is" "blue" "~")) -> ("something" "is" "big" "+"))
All big things are cold.
((("something" "is" "big" "+")) -> ("something" "is" "cold" "+"))
If something is big and furry then it is cold.
((("something" "is" "big" "+") ("something" "is" "furry" "+")) -> ("something" "is" "cold" "+"))
Gary is rough.
True
1
proof
[(triple15)]
("Gary" "is" "rough" "+")
triple15
Gary is not kind.
False
1
inv-proof
[(triple14)]
("Gary" "is" "kind" "-")
triple14
Erin is big.
True
3
proof
[(((triple6 triple5) -> rule4) OR ((triple6 ((triple6 triple7) -> rule3)) -> rule4))]
("Erin" "is" "big" "+")
((triple6 triple5) -> (rule4 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
((triple6 ((triple6 triple7) -> (rule3 % int2))) -> (rule4 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is not blue.
("Erin" "is" "blue" "-")
int2
Erin is not big.
False
3
inv-proof
[(((triple6 triple5) -> rule4) OR ((triple6 ((triple6 triple7) -> rule3)) -> rule4))]
("Erin" "is" "big" "-")
((triple6 triple5) -> (rule4 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
((triple6 ((triple6 triple7) -> (rule3 % int2))) -> (rule4 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is not blue.
("Erin" "is" "blue" "-")
int2
Erin is cold.
True
4
proof
[(((((triple6 triple5) -> rule4)) -> rule5) OR ((((triple6 triple5) -> rule4) triple6) -> rule6) OR ((((triple6 ((triple6 triple7) -> rule3)) -> rule4)) -> rule5) OR ((((triple6 ((triple6 triple7) -> rule3)) -> rule4) triple6) -> rule6))]
("Erin" "is" "cold" "+")
((((triple6 triple5) -> (rule4 % int2))) -> (rule5 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
((((triple6 triple5) -> (rule4 % int2)) triple6) -> (rule6 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
((((triple6 ((triple6 triple7) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is not blue.
("Erin" "is" "blue" "-")
int3
((((triple6 ((triple6 triple7) -> (rule3 % int3))) -> (rule4 % int2)) triple6) -> (rule6 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is not blue.
("Erin" "is" "blue" "-")
int3
Erin is not cold.
False
4
inv-proof
[(((((triple6 triple5) -> rule4)) -> rule5) OR ((((triple6 triple5) -> rule4) triple6) -> rule6) OR ((((triple6 ((triple6 triple7) -> rule3)) -> rule4)) -> rule5) OR ((((triple6 ((triple6 triple7) -> rule3)) -> rule4) triple6) -> rule6))]
("Erin" "is" "cold" "-")
((((triple6 triple5) -> (rule4 % int2))) -> (rule5 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
((((triple6 triple5) -> (rule4 % int2)) triple6) -> (rule6 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
((((triple6 ((triple6 triple7) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is not blue.
("Erin" "is" "blue" "-")
int3
((((triple6 ((triple6 triple7) -> (rule3 % int3))) -> (rule4 % int2)) triple6) -> (rule6 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is not blue.
("Erin" "is" "blue" "-")
int3
Anne is not blue.
Unknown
inv-rconc
[@1: Anne is blue.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Anne" "is" "blue" "-")
Anne is green.
Unknown
random
[@0: Anne is green.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "green" "+")
@0: Anne is big.[(triple1)] Anne is cold.[(triple2 OR ((triple1) -> rule5) OR ((triple1 triple3) -> rule6))] Anne is furry.[(triple3)] Anne is rough.[(triple4)] Erin is furry.[(triple6)] Erin is kind.[(triple8)] Erin is not blue.[(triple5 OR ((triple6 triple7) -> rule3))] Erin is not green.[(triple7)] Erin is rough.[(triple9)] Gary is big.[(triple10)] Gary is cold.[(triple11 OR ((triple10) -> rule5) OR ((triple10 triple12) -> rule6))] Gary is furry.[(triple12)] Gary is green.[(triple13)] Gary is kind.[(triple14)] Gary is rough.[(triple15)] @1: Erin is big.[(((triple6 triple5) -> rule4) OR ((triple6 ((triple6 triple7) -> rule3)) -> rule4))] Gary is blue.[(((triple13) -> rule1))] @2: Erin is cold.[(((((triple6 triple5) -> rule4)) -> rule5) OR ((((triple6 triple5) -> rule4) triple6) -> rule6) OR ((((triple6 ((triple6 triple7) -> rule3)) -> rule4)) -> rule5) OR ((((triple6 ((triple6 triple7) -> rule3)) -> rule4) triple6) -> rule6))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is cold.
("Anne" "is" "cold" "+")
triple2
((triple1) -> (rule5 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
((triple1 triple3) -> (rule6 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
triple3
Anne is rough.
("Anne" "is" "rough" "+")
triple4
Erin is furry.
("Erin" "is" "furry" "+")
triple6
Erin is kind.
("Erin" "is" "kind" "+")
triple8
Erin is not blue.
("Erin" "is" "blue" "-")
triple5
((triple6 triple7) -> (rule3 % int1))
Erin is not blue.
("Erin" "is" "blue" "-")
int1
Erin is not green.
("Erin" "is" "green" "-")
triple7
Erin is rough.
("Erin" "is" "rough" "+")
triple9
Gary is big.
("Gary" "is" "big" "+")
triple10
Gary is cold.
("Gary" "is" "cold" "+")
triple11
((triple10) -> (rule5 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
((triple10 triple12) -> (rule6 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
triple12
Gary is green.
("Gary" "is" "green" "+")
triple13
Gary is kind.
("Gary" "is" "kind" "+")
triple14
Gary is rough.
("Gary" "is" "rough" "+")
triple15
Erin is big.
("Erin" "is" "big" "+")
((triple6 triple5) -> (rule4 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
((triple6 ((triple6 triple7) -> (rule3 % int2))) -> (rule4 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is not blue.
("Erin" "is" "blue" "-")
int2
Gary is blue.
("Gary" "is" "blue" "+")
((triple13) -> (rule1 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
((((triple6 triple5) -> (rule4 % int2))) -> (rule5 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
((((triple6 triple5) -> (rule4 % int2)) triple6) -> (rule6 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
((((triple6 ((triple6 triple7) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is not blue.
("Erin" "is" "blue" "-")
int3
((((triple6 ((triple6 triple7) -> (rule3 % int3))) -> (rule4 % int2)) triple6) -> (rule6 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is not blue.
("Erin" "is" "blue" "-")
int3