Anne is big. Erin is red. Fiona is green. Gary is nice. All quiet things are big. All cold, nice things are red. If something is nice then it is red. If something is red then it is cold. If something is furry then it is cold. If Erin is quiet then Erin is green. All quiet things are furry. If Anne is big then Anne is quiet.
Anne is big.
("Anne" "is" "big" "+")
Erin is red.
("Erin" "is" "red" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Gary is nice.
("Gary" "is" "nice" "+")
All quiet things are big.
((("something" "is" "quiet" "+")) -> ("something" "is" "big" "+"))
All cold, nice things are red.
((("something" "is" "cold" "+") ("something" "is" "nice" "+")) -> ("something" "is" "red" "+"))
If something is nice then it is red.
((("something" "is" "nice" "+")) -> ("something" "is" "red" "+"))
If something is red then it is cold.
((("something" "is" "red" "+")) -> ("something" "is" "cold" "+"))
If something is furry then it is cold.
((("something" "is" "furry" "+")) -> ("something" "is" "cold" "+"))
If Erin is quiet then Erin is green.
((("Erin" "is" "quiet" "+")) -> ("Erin" "is" "green" "+"))
All quiet things are furry.
((("something" "is" "quiet" "+")) -> ("something" "is" "furry" "+"))
If Anne is big then Anne is quiet.
((("Anne" "is" "big" "+")) -> ("Anne" "is" "quiet" "+"))
Fiona is green.
True
1
proof
[(triple3)]
("Fiona" "is" "green" "+")
triple3
Fiona is not green.
False
1
inv-proof
[(triple3)]
("Fiona" "is" "green" "-")
triple3
Erin is cold.
True
2
proof
[(((triple2) -> rule4))]
("Erin" "is" "cold" "+")
((triple2) -> (rule4 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Anne is not quiet.
False
2
inv-proof
[(((triple1) -> rule8))]
("Anne" "is" "quiet" "-")
((triple1) -> (rule8 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is furry.
True
3
proof
[(((((triple1) -> rule8)) -> rule7))]
("Anne" "is" "furry" "+")
((((triple1) -> (rule8 % int2))) -> (rule7 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is not furry.
False
3
inv-proof
[(((((triple1) -> rule8)) -> rule7))]
("Anne" "is" "furry" "-")
((((triple1) -> (rule8 % int2))) -> (rule7 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is cold.
True
4
proof
[(((((((triple1) -> rule8)) -> rule7)) -> rule5))]
("Anne" "is" "cold" "+")
((((((triple1) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3
Anne is not cold.
False
4
inv-proof
[(((((((triple1) -> rule8)) -> rule7)) -> rule5))]
("Anne" "is" "cold" "-")
((((((triple1) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3
Gary is not big.
Unknown
inv-rconc
[@1: Gary is big.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "big" "-")
Anne is red.
Unknown
rconc
[@1: Anne is red.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Anne" "is" "red" "+")
Fiona is not cold.
Unknown
inv-rconc
[@2: Fiona is cold.[CWA. Example of deepest failure = (rule4 <- rule2 <- FAIL)]]
("Fiona" "is" "cold" "-")
Fiona is big.
Unknown
rconc
[@1: Fiona is big.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Fiona" "is" "big" "+")
Fiona is not nice.
Unknown
inv-random
[@0: Fiona is nice.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "nice" "-")
Anne is green.
Unknown
random
[@0: Anne is green.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "green" "+")
Gary is not green.
Unknown
inv-random
[@0: Gary is green.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "green" "-")
Erin is quiet.
Unknown
random
[@0: Erin is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "quiet" "+")
@0: Anne is big.[(triple1)] Erin is red.[(triple2)] Fiona is green.[(triple3)] Gary is nice.[(triple4)] @1: Anne is quiet.[(((triple1) -> rule8))] Erin is cold.[(((triple2) -> rule4))] Gary is red.[(((triple4) -> rule3))] @2: Anne is furry.[(((((triple1) -> rule8)) -> rule7))] Gary is cold.[(((((triple4) -> rule3)) -> rule4))] @3: Anne is cold.[(((((((triple1) -> rule8)) -> rule7)) -> rule5))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Erin is red.
("Erin" "is" "red" "+")
triple2
Fiona is green.
("Fiona" "is" "green" "+")
triple3
Gary is nice.
("Gary" "is" "nice" "+")
triple4
Anne is quiet.
("Anne" "is" "quiet" "+")
((triple1) -> (rule8 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
((triple2) -> (rule4 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
((triple4) -> (rule3 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
((((triple1) -> (rule8 % int2))) -> (rule7 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
((((triple4) -> (rule3 % int2))) -> (rule4 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
((((((triple1) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3