Anne is big. Anne is cold. Dave is big. Erin is big. Erin is cold. Erin is red. Gary is white. All green things are cold. Cold things are red. If Erin is nice then Erin is red. If something is big then it is green. Red things are white. If something is white and big then it is red. If something is white then it is rough. If Anne is rough then Anne is red. All big, nice things are green.
Anne is big.
("Anne" "is" "big" "+")
Anne is cold.
("Anne" "is" "cold" "+")
Dave is big.
("Dave" "is" "big" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is red.
("Erin" "is" "red" "+")
Gary is white.
("Gary" "is" "white" "+")
All green things are cold.
((("something" "is" "green" "+")) -> ("something" "is" "cold" "+"))
Cold things are red.
((("something" "is" "cold" "+")) -> ("something" "is" "red" "+"))
If Erin is nice then Erin is red.
((("Erin" "is" "nice" "+")) -> ("Erin" "is" "red" "+"))
If something is big then it is green.
((("something" "is" "big" "+")) -> ("something" "is" "green" "+"))
Red things are white.
((("something" "is" "red" "+")) -> ("something" "is" "white" "+"))
If something is white and big then it is red.
((("something" "is" "white" "+") ("something" "is" "big" "+")) -> ("something" "is" "red" "+"))
If something is white then it is rough.
((("something" "is" "white" "+")) -> ("something" "is" "rough" "+"))
If Anne is rough then Anne is red.
((("Anne" "is" "rough" "+")) -> ("Anne" "is" "red" "+"))
All big, nice things are green.
((("something" "is" "big" "+") ("something" "is" "nice" "+")) -> ("something" "is" "green" "+"))
Erin is red.
True
1
proof
[(triple6 OR ((triple5) -> rule2) OR ((((((triple4) -> rule4)) -> rule1)) -> rule2))]
("Erin" "is" "red" "+")
triple6
((triple5) -> (rule2 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
((((((triple4) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
Erin is not red.
False
1
inv-proof
[(triple6 OR ((triple5) -> rule2) OR ((((((triple4) -> rule4)) -> rule1)) -> rule2))]
("Erin" "is" "red" "-")
triple6
((triple5) -> (rule2 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
((((((triple4) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
Gary is rough.
True
2
proof
[(((triple7) -> rule7))]
("Gary" "is" "rough" "+")
((triple7) -> (rule7 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Erin is not green.
False
2
inv-proof
[(((triple4) -> rule4))]
("Erin" "is" "green" "-")
((triple4) -> (rule4 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is rough.
True
3
proof
[(((((triple6) -> rule5)) -> rule7) OR ((((((triple5) -> rule2)) -> rule5)) -> rule7) OR ((((((((((triple4) -> rule4)) -> rule1)) -> rule2)) -> rule5)) -> rule7))]
("Erin" "is" "rough" "+")
((((triple6) -> (rule5 % int2))) -> (rule7 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
((((((triple5) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
((((((((((triple4) -> (rule4 % int5))) -> (rule1 % int4))) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
Erin is cold.
("Erin" "is" "cold" "+")
int4
Erin is green.
("Erin" "is" "green" "+")
int5
Anne is not white.
False
3
inv-proof
[(((((triple2) -> rule2)) -> rule5) OR ((((((((triple1) -> rule4)) -> rule1)) -> rule2)) -> rule5))]
("Anne" "is" "white" "-")
((((triple2) -> (rule2 % int2))) -> (rule5 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
((((((((triple1) -> (rule4 % int4))) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
Anne is green.
("Anne" "is" "green" "+")
int4
Anne is rough.
True
4
proof
[(((((((triple2) -> rule2)) -> rule5)) -> rule7) OR ((((((((((triple1) -> rule4)) -> rule1)) -> rule2)) -> rule5)) -> rule7))]
("Anne" "is" "rough" "+")
((((((triple2) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3
((((((((((triple1) -> (rule4 % int5))) -> (rule1 % int4))) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3
Anne is cold.
("Anne" "is" "cold" "+")
int4
Anne is green.
("Anne" "is" "green" "+")
int5
Dave is not red.
False
4
inv-proof
[(((((((triple3) -> rule4)) -> rule1)) -> rule2))]
("Dave" "is" "red" "-")
((((((triple3) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Dave is white.
True
5
proof
[(((((((((triple3) -> rule4)) -> rule1)) -> rule2)) -> rule5))]
("Dave" "is" "white" "+")
((((((((triple3) -> (rule4 % int4))) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
int3
Dave is green.
("Dave" "is" "green" "+")
int4
Dave is not white.
False
5
inv-proof
[(((((((((triple3) -> rule4)) -> rule1)) -> rule2)) -> rule5))]
("Dave" "is" "white" "-")
((((((((triple3) -> (rule4 % int4))) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
int3
Dave is green.
("Dave" "is" "green" "+")
int4
Dave is rough.
True
6
proof
[(((((((((((triple3) -> rule4)) -> rule1)) -> rule2)) -> rule5)) -> rule7))]
("Dave" "is" "rough" "+")
((((((((((triple3) -> (rule4 % int5))) -> (rule1 % int4))) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3
Dave is cold.
("Dave" "is" "cold" "+")
int4
Dave is green.
("Dave" "is" "green" "+")
int5
Dave is not rough.
False
6
inv-proof
[(((((((((((triple3) -> rule4)) -> rule1)) -> rule2)) -> rule5)) -> rule7))]
("Dave" "is" "rough" "-")
((((((((((triple3) -> (rule4 % int5))) -> (rule1 % int4))) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3
Dave is cold.
("Dave" "is" "cold" "+")
int4
Dave is green.
("Dave" "is" "green" "+")
int5
Gary is not cold.
Unknown
inv-rconc
[@2: Gary is cold.[CWA. Example of deepest failure = (rule1 <- rule4 <- FAIL)]]
("Gary" "is" "cold" "-")
Gary is green.
Unknown
rconc
[@1: Gary is green.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Gary" "is" "green" "+")
Gary is not red.
Unknown
inv-rconc
[@3: Gary is red.[CWA. Example of deepest failure = (rule2 <- rule1 <- rule4 <- FAIL)]]
("Gary" "is" "red" "-")
Dave is nice.
Unknown
random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "+")
Anne is not nice.
Unknown
inv-random
[@0: Anne is nice.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "nice" "-")
Gary is big.
Unknown
random
[@0: Gary is big.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "big" "+")
Gary is not nice.
Unknown
inv-random
[@0: Gary is nice.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "nice" "-")
Erin is nice.
Unknown
random
[@0: Erin is nice.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "nice" "+")
@0: Anne is big.[(triple1)] Anne is cold.[(triple2 OR ((((triple1) -> rule4)) -> rule1))] Dave is big.[(triple3)] Erin is big.[(triple4)] Erin is cold.[(triple5 OR ((((triple4) -> rule4)) -> rule1))] Erin is red.[(triple6 OR ((triple5) -> rule2) OR ((((((triple4) -> rule4)) -> rule1)) -> rule2))] Gary is white.[(triple7)] @1: Anne is green.[(((triple1) -> rule4))] Anne is red.[(((triple2) -> rule2) OR ((((((triple1) -> rule4)) -> rule1)) -> rule2))] Dave is green.[(((triple3) -> rule4))] Erin is green.[(((triple4) -> rule4))] Erin is white.[(((triple6) -> rule5) OR ((((triple5) -> rule2)) -> rule5) OR ((((((((triple4) -> rule4)) -> rule1)) -> rule2)) -> rule5))] Gary is rough.[(((triple7) -> rule7))] @2: Anne is white.[(((((triple2) -> rule2)) -> rule5) OR ((((((((triple1) -> rule4)) -> rule1)) -> rule2)) -> rule5))] Dave is cold.[(((((triple3) -> rule4)) -> rule1))] Erin is rough.[(((((triple6) -> rule5)) -> rule7) OR ((((((triple5) -> rule2)) -> rule5)) -> rule7) OR ((((((((((triple4) -> rule4)) -> rule1)) -> rule2)) -> rule5)) -> rule7))] @3: Anne is rough.[(((((((triple2) -> rule2)) -> rule5)) -> rule7) OR ((((((((((triple1) -> rule4)) -> rule1)) -> rule2)) -> rule5)) -> rule7))] Dave is red.[(((((((triple3) -> rule4)) -> rule1)) -> rule2))] @4: Dave is white.[(((((((((triple3) -> rule4)) -> rule1)) -> rule2)) -> rule5))] @5: Dave is rough.[(((((((((((triple3) -> rule4)) -> rule1)) -> rule2)) -> rule5)) -> rule7))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is cold.
("Anne" "is" "cold" "+")
triple2
((((triple1) -> (rule4 % int2))) -> (rule1 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
triple3
Erin is big.
("Erin" "is" "big" "+")
triple4
Erin is cold.
("Erin" "is" "cold" "+")
triple5
((((triple4) -> (rule4 % int2))) -> (rule1 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
triple6
((triple5) -> (rule2 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
((((((triple4) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
Gary is white.
("Gary" "is" "white" "+")
triple7
Anne is green.
("Anne" "is" "green" "+")
((triple1) -> (rule4 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
((triple2) -> (rule2 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
((((((triple1) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
Dave is green.
("Dave" "is" "green" "+")
((triple3) -> (rule4 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
((triple4) -> (rule4 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
((triple6) -> (rule5 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
((((triple5) -> (rule2 % int2))) -> (rule5 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
((((((((triple4) -> (rule4 % int4))) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
Erin is green.
("Erin" "is" "green" "+")
int4
Gary is rough.
("Gary" "is" "rough" "+")
((triple7) -> (rule7 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
((((triple2) -> (rule2 % int2))) -> (rule5 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
((((((((triple1) -> (rule4 % int4))) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
Anne is green.
("Anne" "is" "green" "+")
int4
Dave is cold.
("Dave" "is" "cold" "+")
((((triple3) -> (rule4 % int2))) -> (rule1 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
((((triple6) -> (rule5 % int2))) -> (rule7 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
((((((triple5) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
((((((((((triple4) -> (rule4 % int5))) -> (rule1 % int4))) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
Erin is cold.
("Erin" "is" "cold" "+")
int4
Erin is green.
("Erin" "is" "green" "+")
int5
Anne is rough.
("Anne" "is" "rough" "+")
((((((triple2) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3
((((((((((triple1) -> (rule4 % int5))) -> (rule1 % int4))) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3
Anne is cold.
("Anne" "is" "cold" "+")
int4
Anne is green.
("Anne" "is" "green" "+")
int5
Dave is red.
("Dave" "is" "red" "+")
((((((triple3) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Dave is white.
("Dave" "is" "white" "+")
((((((((triple3) -> (rule4 % int4))) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
int3
Dave is green.
("Dave" "is" "green" "+")
int4
Dave is rough.
("Dave" "is" "rough" "+")
((((((((((triple3) -> (rule4 % int5))) -> (rule1 % int4))) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3
Dave is cold.
("Dave" "is" "cold" "+")
int4
Dave is green.
("Dave" "is" "green" "+")
int5