Anne is blue. Anne is green. Anne is not smart. Bob is not furry. Bob is red. Dave is red. Dave is smart. Erin is blue. Erin is furry. Erin is green. Erin is red. Erin is not young. Red, young things are not blue. Smart things are nice. All furry, young things are nice. If Erin is young and Erin is not smart then Erin is green. If something is nice and red then it is young. If something is young and not nice then it is green.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is not smart.
("Anne" "is" "smart" "-")
Bob is not furry.
("Bob" "is" "furry" "-")
Bob is red.
("Bob" "is" "red" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is not young.
("Erin" "is" "young" "-")
Red, young things are not blue.
((("something" "is" "red" "+") ("something" "is" "young" "+")) -> ("something" "is" "blue" "-"))
Smart things are nice.
((("something" "is" "smart" "+")) -> ("something" "is" "nice" "+"))
All furry, young things are nice.
((("something" "is" "furry" "+") ("something" "is" "young" "+")) -> ("something" "is" "nice" "+"))
If Erin is young and Erin is not smart then Erin is green.
((("Erin" "is" "young" "+") ("Erin" "is" "smart" "~")) -> ("Erin" "is" "green" "+"))
If something is nice and red then it is young.
((("something" "is" "nice" "+") ("something" "is" "red" "+")) -> ("something" "is" "young" "+"))
If something is young and not nice then it is green.
((("something" "is" "young" "+") ("something" "is" "nice" "~")) -> ("something" "is" "green" "+"))
Anne is not smart.
True
1
proof
[(triple3)]
("Anne" "is" "smart" "-")
triple3
Erin is not red.
False
1
inv-proof
[(triple11)]
("Erin" "is" "red" "-")
triple11
Dave is nice.
True
2
proof
[(((triple7) -> rule2))]
("Dave" "is" "nice" "+")
((triple7) -> (rule2 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is not nice.
False
2
inv-proof
[(((triple7) -> rule2))]
("Dave" "is" "nice" "-")
((triple7) -> (rule2 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is young.
True
4
proof
[(((((triple7) -> rule2) triple6) -> rule5))]
("Dave" "is" "young" "+")
((((triple7) -> (rule2 % int2)) triple6) -> (rule5 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is not young.
False
4
inv-proof
[(((((triple7) -> rule2) triple6) -> rule5))]
("Dave" "is" "young" "-")
((((triple7) -> (rule2 % int2)) triple6) -> (rule5 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is not blue.
True
6
proof
[(((triple6 ((((triple7) -> rule2) triple6) -> rule5)) -> rule1))]
("Dave" "is" "blue" "-")
((triple6 ((((triple7) -> (rule2 % int3)) triple6) -> (rule5 % int2))) -> (rule1 % int1))
Dave is not blue.
("Dave" "is" "blue" "-")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Dave is blue.
False
6
inv-proof
[(((triple6 ((((triple7) -> rule2) triple6) -> rule5)) -> rule1))]
("Dave" "is" "blue" "+")
((triple6 ((((triple7) -> (rule2 % int3)) triple6) -> (rule5 % int2))) -> (rule1 % int1))
Dave is not blue.
("Dave" "is" "blue" "-")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Erin is not nice.
Unknown
inv-rconc
[@1: Erin is nice.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Erin" "is" "nice" "-")
Anne is nice.
Unknown
rconc
[@1: Anne is nice.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Anne" "is" "nice" "+")
Bob is not green.
Unknown
inv-rconc
[@1: Bob is green.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Bob" "is" "green" "-")
Anne is young.
Unknown
rconc
[@1: Anne is young.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Anne" "is" "young" "+")
Anne is not furry.
Unknown
inv-random
[@0: Anne is furry.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "furry" "-")
Bob is smart.
Unknown
random
[@0: Bob is smart.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "smart" "+")
Erin is not smart.
Unknown
inv-random
[@0: Erin is smart.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "smart" "-")
Dave is furry.
Unknown
random
[@0: Dave is furry.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "furry" "+")
@0: Anne is blue.[(triple1)] Anne is green.[(triple2)] Anne is not smart.[(triple3)] Bob is not furry.[(triple4)] Bob is red.[(triple5)] Dave is red.[(triple6)] Dave is smart.[(triple7)] Erin is blue.[(triple8)] Erin is furry.[(triple9)] Erin is green.[(triple10)] Erin is not young.[(triple12)] Erin is red.[(triple11)] @1: Dave is nice.[(((triple7) -> rule2))] @2: Dave is young.[(((((triple7) -> rule2) triple6) -> rule5))] @3: Dave is not blue.[(((triple6 ((((triple7) -> rule2) triple6) -> rule5)) -> rule1))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is green.
("Anne" "is" "green" "+")
triple2
Anne is not smart.
("Anne" "is" "smart" "-")
triple3
Bob is not furry.
("Bob" "is" "furry" "-")
triple4
Bob is red.
("Bob" "is" "red" "+")
triple5
Dave is red.
("Dave" "is" "red" "+")
triple6
Dave is smart.
("Dave" "is" "smart" "+")
triple7
Erin is blue.
("Erin" "is" "blue" "+")
triple8
Erin is furry.
("Erin" "is" "furry" "+")
triple9
Erin is green.
("Erin" "is" "green" "+")
triple10
Erin is not young.
("Erin" "is" "young" "-")
triple12
Erin is red.
("Erin" "is" "red" "+")
triple11
Dave is nice.
("Dave" "is" "nice" "+")
((triple7) -> (rule2 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
((((triple7) -> (rule2 % int2)) triple6) -> (rule5 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is not blue.
("Dave" "is" "blue" "-")
((triple6 ((((triple7) -> (rule2 % int3)) triple6) -> (rule5 % int2))) -> (rule1 % int1))
Dave is not blue.
("Dave" "is" "blue" "-")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3