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