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