Anne is blue. Anne is green. Anne is nice. Anne is young. Erin is blue. Erin is nice. Erin is young. If someone is nice then they are big. If Anne is red then Anne is nice. All red, big people are green. If Anne is furry and Anne is big then Anne is nice. If someone is big and blue then they are young. Furry people are nice.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is young.
("Anne" "is" "young" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is young.
("Erin" "is" "young" "+")
If someone is nice then they are big.
((("someone" "is" "nice" "+")) -> ("someone" "is" "big" "+"))
If Anne is red then Anne is nice.
((("Anne" "is" "red" "+")) -> ("Anne" "is" "nice" "+"))
All red, big people are green.
((("someone" "is" "red" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "green" "+"))
If Anne is furry and Anne is big then Anne is nice.
((("Anne" "is" "furry" "+") ("Anne" "is" "big" "+")) -> ("Anne" "is" "nice" "+"))
If someone is big and blue then they are young.
((("someone" "is" "big" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "young" "+"))
Furry people are nice.
((("someone" "is" "furry" "+")) -> ("someone" "is" "nice" "+"))
Erin is young.
True
1
proof
[(triple7 OR ((((triple6) -> rule1) triple5) -> rule5))]
("Erin" "is" "young" "+")
triple7
((((triple6) -> (rule1 % int2)) triple5) -> (rule5 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Anne is not young.
False
1
inv-proof
[(triple4 OR ((((triple3) -> rule1) triple1) -> rule5))]
("Anne" "is" "young" "-")
triple4
((((triple3) -> (rule1 % int2)) triple1) -> (rule5 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Erin is not green.
Unknown
inv-rconc
[@1: Erin is green.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Erin" "is" "green" "-")
Anne is red.
Unknown
random
[@0: Anne is red.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "red" "+")
@0: Anne is blue.[(triple1)] Anne is green.[(triple2)] Anne is nice.[(triple3)] Anne is young.[(triple4 OR ((((triple3) -> rule1) triple1) -> rule5))] Erin is blue.[(triple5)] Erin is nice.[(triple6)] Erin is young.[(triple7 OR ((((triple6) -> rule1) triple5) -> rule5))] @1: Anne is big.[(((triple3) -> rule1))] Erin is big.[(((triple6) -> rule1))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is green.
("Anne" "is" "green" "+")
triple2
Anne is nice.
("Anne" "is" "nice" "+")
triple3
Anne is young.
("Anne" "is" "young" "+")
triple4
((((triple3) -> (rule1 % int2)) triple1) -> (rule5 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
triple5
Erin is nice.
("Erin" "is" "nice" "+")
triple6
Erin is young.
("Erin" "is" "young" "+")
triple7
((((triple6) -> (rule1 % int2)) triple5) -> (rule5 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
((triple3) -> (rule1 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
((triple6) -> (rule1 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1