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