Anne is kind. Anne is nice. Bob is green. Bob is rough. Bob is white. Erin is cold. Erin is kind. Erin is rough. Gary is green. Gary is nice. Gary is white. Smart, white people are green. If Anne is green and Anne is nice then Anne is rough. If someone is smart then they are white. All white, kind people are cold. If Gary is nice then Gary is smart. All rough, nice people are cold. If someone is kind then they are white. If someone is cold then they are smart.
Anne is kind.
("Anne" "is" "kind" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is white.
("Bob" "is" "white" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is white.
("Gary" "is" "white" "+")
Smart, white people are green.
((("someone" "is" "smart" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "green" "+"))
If Anne is green and Anne is nice then Anne is rough.
((("Anne" "is" "green" "+") ("Anne" "is" "nice" "+")) -> ("Anne" "is" "rough" "+"))
If someone is smart then they are white.
((("someone" "is" "smart" "+")) -> ("someone" "is" "white" "+"))
All white, kind people are cold.
((("someone" "is" "white" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "cold" "+"))
If Gary is nice then Gary is smart.
((("Gary" "is" "nice" "+")) -> ("Gary" "is" "smart" "+"))
All rough, nice people are cold.
((("someone" "is" "rough" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "cold" "+"))
If someone is kind then they are white.
((("someone" "is" "kind" "+")) -> ("someone" "is" "white" "+"))
If someone is cold then they are smart.
((("someone" "is" "cold" "+")) -> ("someone" "is" "smart" "+"))
Anne is nice.
True
1
proof
[(triple2)]
("Anne" "is" "nice" "+")
triple2
Erin is not rough.
False
1
inv-proof
[(triple8)]
("Erin" "is" "rough" "-")
triple8
Erin is smart.
True
2
proof
[(((triple6) -> rule8) OR ((((((triple7) -> rule7) triple7) -> rule4)) -> rule8))]
("Erin" "is" "smart" "+")
((triple6) -> (rule8 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
((((((triple7) -> (rule7 % int3)) triple7) -> (rule4 % int2))) -> (rule8 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
int3
Anne is not white.
False
2
inv-proof
[(((triple1) -> rule7))]
("Anne" "is" "white" "-")
((triple1) -> (rule7 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Erin is green.
True
5
proof
[(((((triple6) -> rule8) ((triple7) -> rule7)) -> rule1) OR ((((triple6) -> rule8) ((((triple6) -> rule8)) -> rule3)) -> rule1) OR ((((((((triple7) -> rule7) triple7) -> rule4)) -> rule8) ((triple7) -> rule7)) -> rule1) OR ((((((((triple7) -> rule7) triple7) -> rule4)) -> rule8) ((((triple6) -> rule8)) -> rule3)) -> rule1))]
("Erin" "is" "green" "+")
((((triple6) -> (rule8 % int3)) ((triple7) -> (rule7 % int2))) -> (rule1 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
((((triple6) -> (rule8 % int3)) ((((triple6) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
((((((((triple7) -> (rule7 % int4)) triple7) -> (rule4 % int3))) -> (rule8 % int2)) ((triple7) -> (rule7 % int4))) -> (rule1 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
Erin is white.
("Erin" "is" "white" "+")
int4
((((((((triple7) -> (rule7 % int4)) triple7) -> (rule4 % int3))) -> (rule8 % int2)) ((((triple6) -> (rule8 % int2))) -> (rule3 % int4))) -> (rule1 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
Erin is white.
("Erin" "is" "white" "+")
int4
Anne is not cold.
False
4
inv-proof
[(((((triple1) -> rule7) triple1) -> rule4))]
("Anne" "is" "cold" "-")
((((triple1) -> (rule7 % int2)) triple1) -> (rule4 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is smart.
True
5
proof
[(((((((triple1) -> rule7) triple1) -> rule4)) -> rule8))]
("Anne" "is" "smart" "+")
((((((triple1) -> (rule7 % int3)) triple1) -> (rule4 % int2))) -> (rule8 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3
Anne is not smart.
False
5
inv-proof
[(((((((triple1) -> rule7) triple1) -> rule4)) -> rule8))]
("Anne" "is" "smart" "-")
((((((triple1) -> (rule7 % int3)) triple1) -> (rule4 % int2))) -> (rule8 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3
Anne is green.
True
8
proof
[(((((((((triple1) -> rule7) triple1) -> rule4)) -> rule8) ((triple1) -> rule7)) -> rule1))]
("Anne" "is" "green" "+")
((((((((triple1) -> (rule7 % int4)) triple1) -> (rule4 % int3))) -> (rule8 % int2)) ((triple1) -> (rule7 % int4))) -> (rule1 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
Anne is white.
("Anne" "is" "white" "+")
int4
Anne is not green.
False
8
inv-proof
[(((((((((triple1) -> rule7) triple1) -> rule4)) -> rule8) ((triple1) -> rule7)) -> rule1))]
("Anne" "is" "green" "-")
((((((((triple1) -> (rule7 % int4)) triple1) -> (rule4 % int3))) -> (rule8 % int2)) ((triple1) -> (rule7 % int4))) -> (rule1 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
Anne is white.
("Anne" "is" "white" "+")
int4
Anne is rough.
True
10
proof
[(((((((((((triple1) -> rule7) triple1) -> rule4)) -> rule8) ((triple1) -> rule7)) -> rule1) triple2) -> rule2))]
("Anne" "is" "rough" "+")
((((((((((triple1) -> (rule7 % int5)) triple1) -> (rule4 % int4))) -> (rule8 % int3)) ((triple1) -> (rule7 % int5))) -> (rule1 % int2)) triple2) -> (rule2 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Anne is cold.
("Anne" "is" "cold" "+")
int4
Anne is white.
("Anne" "is" "white" "+")
int5
Anne is not rough.
False
10
inv-proof
[(((((((((((triple1) -> rule7) triple1) -> rule4)) -> rule8) ((triple1) -> rule7)) -> rule1) triple2) -> rule2))]
("Anne" "is" "rough" "-")
((((((((((triple1) -> (rule7 % int5)) triple1) -> (rule4 % int4))) -> (rule8 % int3)) ((triple1) -> (rule7 % int5))) -> (rule1 % int2)) triple2) -> (rule2 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Anne is cold.
("Anne" "is" "cold" "+")
int4
Anne is white.
("Anne" "is" "white" "+")
int5
Bob is not smart.
Unknown
inv-rconc
[@2: Bob is smart.[CWA. Example of deepest failure = (rule8 <- rule4 <- FAIL)]]
("Bob" "is" "smart" "-")
Bob is cold.
Unknown
rconc
[@1: Bob is cold.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Bob" "is" "cold" "+")
Gary is not cold.
Unknown
inv-rconc
[@1: Gary is cold.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Gary" "is" "cold" "-")
Gary is kind.
Unknown
random
[@0: Gary is kind.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "kind" "+")
Bob is not nice.
Unknown
inv-random
[@0: Bob is nice.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "nice" "-")
Bob is kind.
Unknown
random
[@0: Bob is kind.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "kind" "+")
Erin is not nice.
Unknown
inv-random
[@0: Erin is nice.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "nice" "-")
Gary is rough.
Unknown
random
[@0: Gary is rough.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "rough" "+")
@0: Anne is kind.[(triple1)] Anne is nice.[(triple2)] Bob is green.[(triple3)] Bob is rough.[(triple4)] Bob is white.[(triple5)] Erin is cold.[(triple6 OR ((((triple7) -> rule7) triple7) -> rule4))] Erin is kind.[(triple7)] Erin is rough.[(triple8)] Gary is green.[(triple9 OR ((((triple10) -> rule5) triple11) -> rule1) OR ((((triple10) -> rule5) ((((triple10) -> rule5)) -> rule3)) -> rule1))] Gary is nice.[(triple10)] Gary is white.[(triple11 OR ((((triple10) -> rule5)) -> rule3))] @1: Anne is white.[(((triple1) -> rule7))] Erin is smart.[(((triple6) -> rule8) OR ((((((triple7) -> rule7) triple7) -> rule4)) -> rule8))] Erin is white.[(((triple7) -> rule7) OR ((((triple6) -> rule8)) -> rule3))] Gary is smart.[(((triple10) -> rule5))] @2: Anne is cold.[(((((triple1) -> rule7) triple1) -> rule4))] Erin is green.[(((((triple6) -> rule8) ((triple7) -> rule7)) -> rule1) OR ((((triple6) -> rule8) ((((triple6) -> rule8)) -> rule3)) -> rule1) OR ((((((((triple7) -> rule7) triple7) -> rule4)) -> rule8) ((triple7) -> rule7)) -> rule1) OR ((((((((triple7) -> rule7) triple7) -> rule4)) -> rule8) ((((triple6) -> rule8)) -> rule3)) -> rule1))] @3: Anne is smart.[(((((((triple1) -> rule7) triple1) -> rule4)) -> rule8))] @4: Anne is green.[(((((((((triple1) -> rule7) triple1) -> rule4)) -> rule8) ((triple1) -> rule7)) -> rule1))] @5: Anne is rough.[(((((((((((triple1) -> rule7) triple1) -> rule4)) -> rule8) ((triple1) -> rule7)) -> rule1) triple2) -> rule2))]
Anne is kind.
("Anne" "is" "kind" "+")
triple1
Anne is nice.
("Anne" "is" "nice" "+")
triple2
Bob is green.
("Bob" "is" "green" "+")
triple3
Bob is rough.
("Bob" "is" "rough" "+")
triple4
Bob is white.
("Bob" "is" "white" "+")
triple5
Erin is cold.
("Erin" "is" "cold" "+")
triple6
((((triple7) -> (rule7 % int2)) triple7) -> (rule4 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
triple7
Erin is rough.
("Erin" "is" "rough" "+")
triple8
Gary is green.
("Gary" "is" "green" "+")
triple9
((((triple10) -> (rule5 % int2)) triple11) -> (rule1 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
((((triple10) -> (rule5 % int3)) ((((triple10) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Gary is nice.
("Gary" "is" "nice" "+")
triple10
Gary is white.
("Gary" "is" "white" "+")
triple11
((((triple10) -> (rule5 % int2))) -> (rule3 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
((triple1) -> (rule7 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
((triple6) -> (rule8 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
((((((triple7) -> (rule7 % int3)) triple7) -> (rule4 % int2))) -> (rule8 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
int3
Erin is white.
("Erin" "is" "white" "+")
((triple7) -> (rule7 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
((((triple6) -> (rule8 % int2))) -> (rule3 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
((triple10) -> (rule5 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
((((triple1) -> (rule7 % int2)) triple1) -> (rule4 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
((((triple6) -> (rule8 % int3)) ((triple7) -> (rule7 % int2))) -> (rule1 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
((((triple6) -> (rule8 % int3)) ((((triple6) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
((((((((triple7) -> (rule7 % int4)) triple7) -> (rule4 % int3))) -> (rule8 % int2)) ((triple7) -> (rule7 % int4))) -> (rule1 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
Erin is white.
("Erin" "is" "white" "+")
int4
((((((((triple7) -> (rule7 % int4)) triple7) -> (rule4 % int3))) -> (rule8 % int2)) ((((triple6) -> (rule8 % int2))) -> (rule3 % int4))) -> (rule1 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
Erin is white.
("Erin" "is" "white" "+")
int4
Anne is smart.
("Anne" "is" "smart" "+")
((((((triple1) -> (rule7 % int3)) triple1) -> (rule4 % int2))) -> (rule8 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3
Anne is green.
("Anne" "is" "green" "+")
((((((((triple1) -> (rule7 % int4)) triple1) -> (rule4 % int3))) -> (rule8 % int2)) ((triple1) -> (rule7 % int4))) -> (rule1 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
Anne is white.
("Anne" "is" "white" "+")
int4
Anne is rough.
("Anne" "is" "rough" "+")
((((((((((triple1) -> (rule7 % int5)) triple1) -> (rule4 % int4))) -> (rule8 % int3)) ((triple1) -> (rule7 % int5))) -> (rule1 % int2)) triple2) -> (rule2 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Anne is cold.
("Anne" "is" "cold" "+")
int4
Anne is white.
("Anne" "is" "white" "+")
int5