Anne is blue. Anne is green. Anne is nice. Anne is red. Anne is smart. Anne is white. Anne is young. Erin is blue. Erin is green. Erin is nice. Erin is red. Erin is smart. Erin is white. Erin is young. If something is red then it is young. Young things are white.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Anne is white.
("Anne" "is" "white" "+")
Anne is young.
("Anne" "is" "young" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Erin is white.
("Erin" "is" "white" "+")
Erin is young.
("Erin" "is" "young" "+")
If something is red then it is young.
((("something" "is" "red" "+")) -> ("something" "is" "young" "+"))
Young things are white.
((("something" "is" "young" "+")) -> ("something" "is" "white" "+"))
Anne is nice.
True
1
proof
[(triple3)]
("Anne" "is" "nice" "+")
triple3
Erin is not nice.
False
1
inv-proof
[(triple10)]
("Erin" "is" "nice" "-")
triple10
@0: Anne is blue.[(triple1)] Anne is green.[(triple2)] Anne is nice.[(triple3)] Anne is red.[(triple4)] Anne is smart.[(triple5)] Anne is white.[(triple6 OR ((triple7) -> rule2) OR ((((triple4) -> rule1)) -> rule2))] Anne is young.[(triple7 OR ((triple4) -> rule1))] Erin is blue.[(triple8)] Erin is green.[(triple9)] Erin is nice.[(triple10)] Erin is red.[(triple11)] Erin is smart.[(triple12)] Erin is white.[(triple13 OR ((triple14) -> rule2) OR ((((triple11) -> rule1)) -> rule2))] Erin is young.[(triple14 OR ((triple11) -> rule1))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is green.
("Anne" "is" "green" "+")
triple2
Anne is nice.
("Anne" "is" "nice" "+")
triple3
Anne is red.
("Anne" "is" "red" "+")
triple4
Anne is smart.
("Anne" "is" "smart" "+")
triple5
Anne is white.
("Anne" "is" "white" "+")
triple6
((triple7) -> (rule2 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
((((triple4) -> (rule1 % int2))) -> (rule2 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
triple7
((triple4) -> (rule1 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
triple8
Erin is green.
("Erin" "is" "green" "+")
triple9
Erin is nice.
("Erin" "is" "nice" "+")
triple10
Erin is red.
("Erin" "is" "red" "+")
triple11
Erin is smart.
("Erin" "is" "smart" "+")
triple12
Erin is white.
("Erin" "is" "white" "+")
triple13
((triple14) -> (rule2 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
((((triple11) -> (rule1 % int2))) -> (rule2 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
triple14
((triple11) -> (rule1 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1