Anne is big. Anne is quiet. Erin is not cold. Erin is green. Erin is not quiet. Fiona is red. Harry is big. If Anne is green then Anne is cold. If someone is red then they are nice. If someone is white and big then they are nice. All red, big people are nice. Quiet, big people are green. All red people are big. If Fiona is green then Fiona is quiet. All cold, green people are red. Nice people are white.
Anne is big.
("Anne" "is" "big" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Erin is not cold.
("Erin" "is" "cold" "-")
Erin is green.
("Erin" "is" "green" "+")
Erin is not quiet.
("Erin" "is" "quiet" "-")
Fiona is red.
("Fiona" "is" "red" "+")
Harry is big.
("Harry" "is" "big" "+")
If Anne is green then Anne is cold.
((("Anne" "is" "green" "+")) -> ("Anne" "is" "cold" "+"))
If someone is red then they are nice.
((("someone" "is" "red" "+")) -> ("someone" "is" "nice" "+"))
If someone is white and big then they are nice.
((("someone" "is" "white" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "nice" "+"))
All red, big people are nice.
((("someone" "is" "red" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "nice" "+"))
Quiet, big people are green.
((("someone" "is" "quiet" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "green" "+"))
All red people are big.
((("someone" "is" "red" "+")) -> ("someone" "is" "big" "+"))
If Fiona is green then Fiona is quiet.
((("Fiona" "is" "green" "+")) -> ("Fiona" "is" "quiet" "+"))
All cold, green people are red.
((("someone" "is" "cold" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "red" "+"))
Nice people are white.
((("someone" "is" "nice" "+")) -> ("someone" "is" "white" "+"))
Fiona is red.
True
1
proof
[(triple6)]
("Fiona" "is" "red" "+")
triple6
Erin is quiet.
False
1
inv-proof
[(triple5)]
("Erin" "is" "quiet" "+")
triple5
Fiona is nice.
True
2
proof
[(((triple6) -> rule2) OR ((triple6 ((triple6) -> rule6)) -> rule4))]
("Fiona" "is" "nice" "+")
((triple6) -> (rule2 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
((triple6 ((triple6) -> (rule6 % int2))) -> (rule4 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Anne is not green.
False
3
inv-proof
[(((triple2 triple1) -> rule5))]
("Anne" "is" "green" "-")
((triple2 triple1) -> (rule5 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is cold.
True
4
proof
[(((((triple2 triple1) -> rule5)) -> rule1))]
("Anne" "is" "cold" "+")
((((triple2 triple1) -> (rule5 % int2))) -> (rule1 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is not cold.
False
4
inv-proof
[(((((triple2 triple1) -> rule5)) -> rule1))]
("Anne" "is" "cold" "-")
((((triple2 triple1) -> (rule5 % int2))) -> (rule1 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is red.
True
8
proof
[(((((((triple2 triple1) -> rule5)) -> rule1) ((triple2 triple1) -> rule5)) -> rule8))]
("Anne" "is" "red" "+")
((((((triple2 triple1) -> (rule5 % int3))) -> (rule1 % int2)) ((triple2 triple1) -> (rule5 % int3))) -> (rule8 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
Anne is not red.
False
8
inv-proof
[(((((((triple2 triple1) -> rule5)) -> rule1) ((triple2 triple1) -> rule5)) -> rule8))]
("Anne" "is" "red" "-")
((((((triple2 triple1) -> (rule5 % int3))) -> (rule1 % int2)) ((triple2 triple1) -> (rule5 % int3))) -> (rule8 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
Anne is nice.
True
9
proof
[(((((((((triple2 triple1) -> rule5)) -> rule1) ((triple2 triple1) -> rule5)) -> rule8)) -> rule2) OR ((((((((triple2 triple1) -> rule5)) -> rule1) ((triple2 triple1) -> rule5)) -> rule8) triple1) -> rule4))]
("Anne" "is" "nice" "+")
((((((((triple2 triple1) -> (rule5 % int4))) -> (rule1 % int3)) ((triple2 triple1) -> (rule5 % int4))) -> (rule8 % int2))) -> (rule2 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
Anne is green.
("Anne" "is" "green" "+")
int4
((((((((triple2 triple1) -> (rule5 % int4))) -> (rule1 % int3)) ((triple2 triple1) -> (rule5 % int4))) -> (rule8 % int2)) triple1) -> (rule4 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
Anne is green.
("Anne" "is" "green" "+")
int4
Anne is not nice.
False
9
inv-proof
[(((((((((triple2 triple1) -> rule5)) -> rule1) ((triple2 triple1) -> rule5)) -> rule8)) -> rule2) OR ((((((((triple2 triple1) -> rule5)) -> rule1) ((triple2 triple1) -> rule5)) -> rule8) triple1) -> rule4))]
("Anne" "is" "nice" "-")
((((((((triple2 triple1) -> (rule5 % int4))) -> (rule1 % int3)) ((triple2 triple1) -> (rule5 % int4))) -> (rule8 % int2))) -> (rule2 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
Anne is green.
("Anne" "is" "green" "+")
int4
((((((((triple2 triple1) -> (rule5 % int4))) -> (rule1 % int3)) ((triple2 triple1) -> (rule5 % int4))) -> (rule8 % int2)) triple1) -> (rule4 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
Anne is green.
("Anne" "is" "green" "+")
int4
Anne is white.
True
10
proof
[(((((((((((triple2 triple1) -> rule5)) -> rule1) ((triple2 triple1) -> rule5)) -> rule8)) -> rule2)) -> rule9) OR ((((((((((triple2 triple1) -> rule5)) -> rule1) ((triple2 triple1) -> rule5)) -> rule8) triple1) -> rule4)) -> rule9))]
("Anne" "is" "white" "+")
((((((((((triple2 triple1) -> (rule5 % int5))) -> (rule1 % int4)) ((triple2 triple1) -> (rule5 % int5))) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule9 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3
Anne is cold.
("Anne" "is" "cold" "+")
int4
Anne is green.
("Anne" "is" "green" "+")
int5
((((((((((triple2 triple1) -> (rule5 % int5))) -> (rule1 % int4)) ((triple2 triple1) -> (rule5 % int5))) -> (rule8 % int3)) triple1) -> (rule4 % int2))) -> (rule9 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3
Anne is cold.
("Anne" "is" "cold" "+")
int4
Anne is green.
("Anne" "is" "green" "+")
int5
Anne is not white.
False
10
inv-proof
[(((((((((((triple2 triple1) -> rule5)) -> rule1) ((triple2 triple1) -> rule5)) -> rule8)) -> rule2)) -> rule9) OR ((((((((((triple2 triple1) -> rule5)) -> rule1) ((triple2 triple1) -> rule5)) -> rule8) triple1) -> rule4)) -> rule9))]
("Anne" "is" "white" "-")
((((((((((triple2 triple1) -> (rule5 % int5))) -> (rule1 % int4)) ((triple2 triple1) -> (rule5 % int5))) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule9 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3
Anne is cold.
("Anne" "is" "cold" "+")
int4
Anne is green.
("Anne" "is" "green" "+")
int5
((((((((((triple2 triple1) -> (rule5 % int5))) -> (rule1 % int4)) ((triple2 triple1) -> (rule5 % int5))) -> (rule8 % int3)) triple1) -> (rule4 % int2))) -> (rule9 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3
Anne is cold.
("Anne" "is" "cold" "+")
int4
Anne is green.
("Anne" "is" "green" "+")
int5
Harry is not nice.
Unknown
inv-rconc
[@4: Harry is nice.[CWA. Example of deepest failure = (rule3 <- rule9 <- rule2 <- rule8 <- FAIL)]]
("Harry" "is" "nice" "-")
Erin is nice.
Unknown
rconc
[@3: Erin is nice.[CWA. Example of deepest failure = (rule3 <- rule6 <- rule8 <- FAIL)]]
("Erin" "is" "nice" "+")
Erin is not big.
Unknown
inv-rconc
[@2: Erin is big.[CWA. Example of deepest failure = (rule6 <- rule8 <- FAIL)]]
("Erin" "is" "big" "-")
Erin is white.
Unknown
rconc
[@3: Erin is white.[CWA. Example of deepest failure = (rule9 <- rule2 <- rule8 <- FAIL)]]
("Erin" "is" "white" "+")
Harry is not red.
Unknown
inv-rconc
[@1: Harry is red.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Harry" "is" "red" "-")
Harry is green.
Unknown
rconc
[@1: Harry is green.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Harry" "is" "green" "+")
Harry is not cold.
Unknown
inv-random
[@0: Harry is cold.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "cold" "-")
Harry is quiet.
Unknown
random
[@0: Harry is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "quiet" "+")
@0: Anne is big.[(triple1)] Anne is quiet.[(triple2)] Erin is green.[(triple4)] Erin is not cold.[(triple3)] Erin is not quiet.[(triple5)] Fiona is red.[(triple6)] Harry is big.[(triple7)] @1: Anne is green.[(((triple2 triple1) -> rule5))] Fiona is big.[(((triple6) -> rule6))] Fiona is nice.[(((triple6) -> rule2) OR ((triple6 ((triple6) -> rule6)) -> rule4))] @2: Anne is cold.[(((((triple2 triple1) -> rule5)) -> rule1))] Fiona is white.[(((((triple6) -> rule2)) -> rule9) OR ((((triple6 ((triple6) -> rule6)) -> rule4)) -> rule9))] @3: Anne is red.[(((((((triple2 triple1) -> rule5)) -> rule1) ((triple2 triple1) -> rule5)) -> rule8))] @4: Anne is nice.[(((((((((triple2 triple1) -> rule5)) -> rule1) ((triple2 triple1) -> rule5)) -> rule8)) -> rule2) OR ((((((((triple2 triple1) -> rule5)) -> rule1) ((triple2 triple1) -> rule5)) -> rule8) triple1) -> rule4))] @5: Anne is white.[(((((((((((triple2 triple1) -> rule5)) -> rule1) ((triple2 triple1) -> rule5)) -> rule8)) -> rule2)) -> rule9) OR ((((((((((triple2 triple1) -> rule5)) -> rule1) ((triple2 triple1) -> rule5)) -> rule8) triple1) -> rule4)) -> rule9))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is quiet.
("Anne" "is" "quiet" "+")
triple2
Erin is green.
("Erin" "is" "green" "+")
triple4
Erin is not cold.
("Erin" "is" "cold" "-")
triple3
Erin is not quiet.
("Erin" "is" "quiet" "-")
triple5
Fiona is red.
("Fiona" "is" "red" "+")
triple6
Harry is big.
("Harry" "is" "big" "+")
triple7
Anne is green.
("Anne" "is" "green" "+")
((triple2 triple1) -> (rule5 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
((triple6) -> (rule6 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
((triple6) -> (rule2 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
((triple6 ((triple6) -> (rule6 % int2))) -> (rule4 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
((((triple2 triple1) -> (rule5 % int2))) -> (rule1 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Fiona is white.
("Fiona" "is" "white" "+")
((((triple6) -> (rule2 % int2))) -> (rule9 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
((((triple6 ((triple6) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule9 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Fiona is big.
("Fiona" "is" "big" "+")
int3
Anne is red.
("Anne" "is" "red" "+")
((((((triple2 triple1) -> (rule5 % int3))) -> (rule1 % int2)) ((triple2 triple1) -> (rule5 % int3))) -> (rule8 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
Anne is nice.
("Anne" "is" "nice" "+")
((((((((triple2 triple1) -> (rule5 % int4))) -> (rule1 % int3)) ((triple2 triple1) -> (rule5 % int4))) -> (rule8 % int2))) -> (rule2 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
Anne is green.
("Anne" "is" "green" "+")
int4
((((((((triple2 triple1) -> (rule5 % int4))) -> (rule1 % int3)) ((triple2 triple1) -> (rule5 % int4))) -> (rule8 % int2)) triple1) -> (rule4 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
Anne is green.
("Anne" "is" "green" "+")
int4
Anne is white.
("Anne" "is" "white" "+")
((((((((((triple2 triple1) -> (rule5 % int5))) -> (rule1 % int4)) ((triple2 triple1) -> (rule5 % int5))) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule9 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3
Anne is cold.
("Anne" "is" "cold" "+")
int4
Anne is green.
("Anne" "is" "green" "+")
int5
((((((((((triple2 triple1) -> (rule5 % int5))) -> (rule1 % int4)) ((triple2 triple1) -> (rule5 % int5))) -> (rule8 % int3)) triple1) -> (rule4 % int2))) -> (rule9 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3
Anne is cold.
("Anne" "is" "cold" "+")
int4
Anne is green.
("Anne" "is" "green" "+")
int5