Anne is big. Anne is kind. Anne is red. Anne is round. Erin is big. Erin is not blue. Erin is green. Erin is kind. Erin is not round. Erin is not white. All kind, big things are not white. White things are big. All kind things are green. All green things are not blue. All big, blue things are kind. If Erin is blue then Erin is green.
Anne is big.
("Anne" "is" "big" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is round.
("Anne" "is" "round" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is not blue.
("Erin" "is" "blue" "-")
Erin is green.
("Erin" "is" "green" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is not round.
("Erin" "is" "round" "-")
Erin is not white.
("Erin" "is" "white" "-")
All kind, big things are not white.
((("something" "is" "kind" "+") ("something" "is" "big" "+")) -> ("something" "is" "white" "-"))
White things are big.
((("something" "is" "white" "+")) -> ("something" "is" "big" "+"))
All kind things are green.
((("something" "is" "kind" "+")) -> ("something" "is" "green" "+"))
All green things are not blue.
((("something" "is" "green" "+")) -> ("something" "is" "blue" "-"))
All big, blue things are kind.
((("something" "is" "big" "+") ("something" "is" "blue" "+")) -> ("something" "is" "kind" "+"))
If Erin is blue then Erin is green.
((("Erin" "is" "blue" "+")) -> ("Erin" "is" "green" "+"))
Erin is not round.
True
1
proof
[(triple9)]
("Erin" "is" "round" "-")
triple9
Erin is blue.
False
1
inv-proof
[(triple6 OR ((triple7) -> rule4) OR ((((triple8) -> rule3)) -> rule4))]
("Erin" "is" "blue" "+")
triple6
((triple7) -> (rule4 % int1))
Erin is not blue.
("Erin" "is" "blue" "-")
int1
((((triple8) -> (rule3 % int2))) -> (rule4 % int1))
Erin is not blue.
("Erin" "is" "blue" "-")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Anne is not white.
True
3
proof
[(((triple2 triple1) -> rule1))]
("Anne" "is" "white" "-")
((triple2 triple1) -> (rule1 % int1))
Anne is not white.
("Anne" "is" "white" "-")
int1
Anne is not green.
False
2
inv-proof
[(((triple2) -> rule3))]
("Anne" "is" "green" "-")
((triple2) -> (rule3 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
@0: Anne is big.[(triple1)] Anne is kind.[(triple2)] Anne is red.[(triple3)] Anne is round.[(triple4)] Erin is big.[(triple5)] Erin is green.[(triple7 OR ((triple8) -> rule3))] Erin is kind.[(triple8)] Erin is not blue.[(triple6 OR ((triple7) -> rule4) OR ((((triple8) -> rule3)) -> rule4))] Erin is not round.[(triple9)] Erin is not white.[(triple10 OR ((triple8 triple5) -> rule1))] @1: Anne is green.[(((triple2) -> rule3))] Anne is not white.[(((triple2 triple1) -> rule1))] @2: Anne is not blue.[(((((triple2) -> rule3)) -> rule4))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is kind.
("Anne" "is" "kind" "+")
triple2
Anne is red.
("Anne" "is" "red" "+")
triple3
Anne is round.
("Anne" "is" "round" "+")
triple4
Erin is big.
("Erin" "is" "big" "+")
triple5
Erin is green.
("Erin" "is" "green" "+")
triple7
((triple8) -> (rule3 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
triple8
Erin is not blue.
("Erin" "is" "blue" "-")
triple6
((triple7) -> (rule4 % int1))
Erin is not blue.
("Erin" "is" "blue" "-")
int1
((((triple8) -> (rule3 % int2))) -> (rule4 % int1))
Erin is not blue.
("Erin" "is" "blue" "-")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is not round.
("Erin" "is" "round" "-")
triple9
Erin is not white.
("Erin" "is" "white" "-")
triple10
((triple8 triple5) -> (rule1 % int1))
Erin is not white.
("Erin" "is" "white" "-")
int1
Anne is green.
("Anne" "is" "green" "+")
((triple2) -> (rule3 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is not white.
("Anne" "is" "white" "-")
((triple2 triple1) -> (rule1 % int1))
Anne is not white.
("Anne" "is" "white" "-")
int1
Anne is not blue.
("Anne" "is" "blue" "-")
((((triple2) -> (rule3 % int2))) -> (rule4 % int1))
Anne is not blue.
("Anne" "is" "blue" "-")
int1
Anne is green.
("Anne" "is" "green" "+")
int2