Anne is not blue. Anne is not red. Anne is not round. Anne is white. Bob is young. Erin is green. Erin is young. All white things are green. If something is nice and not green then it is red. If something is young and round then it is not red. If something is round and not blue then it is not young. If something is green then it is young. If something is white and red then it is young. Young things are nice. If something is green and red then it is nice.
Anne is not blue.
("Anne" "is" "blue" "-")
Anne is not red.
("Anne" "is" "red" "-")
Anne is not round.
("Anne" "is" "round" "-")
Anne is white.
("Anne" "is" "white" "+")
Bob is young.
("Bob" "is" "young" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is young.
("Erin" "is" "young" "+")
All white things are green.
((("something" "is" "white" "+")) -> ("something" "is" "green" "+"))
If something is nice and not green then it is red.
((("something" "is" "nice" "+") ("something" "is" "green" "~")) -> ("something" "is" "red" "+"))
If something is young and round then it is not red.
((("something" "is" "young" "+") ("something" "is" "round" "+")) -> ("something" "is" "red" "-"))
If something is round and not blue then it is not young.
((("something" "is" "round" "+") ("something" "is" "blue" "~")) -> ("something" "is" "young" "-"))
If something is green then it is young.
((("something" "is" "green" "+")) -> ("something" "is" "young" "+"))
If something is white and red then it is young.
((("something" "is" "white" "+") ("something" "is" "red" "+")) -> ("something" "is" "young" "+"))
Young things are nice.
((("something" "is" "young" "+")) -> ("something" "is" "nice" "+"))
If something is green and red then it is nice.
((("something" "is" "green" "+") ("something" "is" "red" "+")) -> ("something" "is" "nice" "+"))
Anne is not blue.
True
1
proof
[(triple1)]
("Anne" "is" "blue" "-")
triple1
Anne is blue.
False
1
inv-proof
[(triple1)]
("Anne" "is" "blue" "+")
triple1
Anne is green.
True
2
proof
[(((triple4) -> rule1))]
("Anne" "is" "green" "+")
((triple4) -> (rule1 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is not green.
False
2
inv-proof
[(((triple4) -> rule1))]
("Anne" "is" "green" "-")
((triple4) -> (rule1 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is young.
True
3
proof
[(((((triple4) -> rule1)) -> rule5))]
("Anne" "is" "young" "+")
((((triple4) -> (rule1 % int2))) -> (rule5 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is not young.
False
3
inv-proof
[(((((triple4) -> rule1)) -> rule5))]
("Anne" "is" "young" "-")
((((triple4) -> (rule1 % int2))) -> (rule5 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is nice.
True
4
proof
[(((((((triple4) -> rule1)) -> rule5)) -> rule7))]
("Anne" "is" "nice" "+")
((((((triple4) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
Anne is not nice.
False
4
inv-proof
[(((((((triple4) -> rule1)) -> rule5)) -> rule7))]
("Anne" "is" "nice" "-")
((((((triple4) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
Bob is not green.
Unknown
inv-rconc
[@1: Bob is green.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "green" "-")
Bob is red.
Unknown
rconc
[@1: Bob is red.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "red" "+")
Erin is not red.
Unknown
inv-rconc
[@1: Erin is red.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Erin" "is" "red" "-")
Bob is round.
Unknown
random
[@0: Bob is round.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "round" "+")
Erin is not blue.
Unknown
inv-random
[@0: Erin is blue.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "blue" "-")
Erin is round.
Unknown
random
[@0: Erin is round.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "round" "+")
Erin is not white.
Unknown
inv-random
[@0: Erin is white.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "white" "-")
Bob is white.
Unknown
random
[@0: Bob is white.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "white" "+")
@0: Anne is not blue.[(triple1)] Anne is not red.[(triple2)] Anne is not round.[(triple3)] Anne is white.[(triple4)] Bob is young.[(triple5)] Erin is green.[(triple6)] Erin is young.[(triple7 OR ((triple6) -> rule5))] @1: Anne is green.[(((triple4) -> rule1))] Bob is nice.[(((triple5) -> rule7))] Erin is nice.[(((triple7) -> rule7) OR ((((triple6) -> rule5)) -> rule7))] @2: Anne is young.[(((((triple4) -> rule1)) -> rule5))] @3: Anne is nice.[(((((((triple4) -> rule1)) -> rule5)) -> rule7))]
Anne is not blue.
("Anne" "is" "blue" "-")
triple1
Anne is not red.
("Anne" "is" "red" "-")
triple2
Anne is not round.
("Anne" "is" "round" "-")
triple3
Anne is white.
("Anne" "is" "white" "+")
triple4
Bob is young.
("Bob" "is" "young" "+")
triple5
Erin is green.
("Erin" "is" "green" "+")
triple6
Erin is young.
("Erin" "is" "young" "+")
triple7
((triple6) -> (rule5 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
((triple4) -> (rule1 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
((triple5) -> (rule7 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
((triple7) -> (rule7 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
((((triple6) -> (rule5 % int2))) -> (rule7 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
((((triple4) -> (rule1 % int2))) -> (rule5 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
((((((triple4) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3