Erin is big. Erin is furry. Erin is green. Erin is kind. Erin is quiet. Erin is red. Erin is white. Big, quiet things are kind. Big things are white. If Erin is red and Erin is kind then Erin is quiet. All big things are kind. Big, green things are white. All kind, white things are green.
Erin is big.
("Erin" "is" "big" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is white.
("Erin" "is" "white" "+")
Big, quiet things are kind.
((("something" "is" "big" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "kind" "+"))
Big things are white.
((("something" "is" "big" "+")) -> ("something" "is" "white" "+"))
If Erin is red and Erin is kind then Erin is quiet.
((("Erin" "is" "red" "+") ("Erin" "is" "kind" "+")) -> ("Erin" "is" "quiet" "+"))
All big things are kind.
((("something" "is" "big" "+")) -> ("something" "is" "kind" "+"))
Big, green things are white.
((("something" "is" "big" "+") ("something" "is" "green" "+")) -> ("something" "is" "white" "+"))
All kind, white things are green.
((("something" "is" "kind" "+") ("something" "is" "white" "+")) -> ("something" "is" "green" "+"))
Erin is red.
True
1
proof
[(triple6)]
("Erin" "is" "red" "+")
triple6
Erin is not red.
False
1
inv-proof
[(triple6)]
("Erin" "is" "red" "-")
triple6
@0: Erin is big.[(triple1)] Erin is furry.[(triple2)] Erin is green.[(triple3 OR ((triple4 triple7) -> rule6) OR ((triple4 ((triple1) -> rule2)) -> rule6) OR ((((triple1) -> rule4) triple7) -> rule6) OR ((((triple1 triple5) -> rule1) triple7) -> rule6) OR ((((triple1) -> rule4) ((triple1) -> rule2)) -> rule6) OR ((((triple1 triple5) -> rule1) ((triple1) -> rule2)) -> rule6))] Erin is kind.[(triple4 OR ((triple1) -> rule4) OR ((triple1 triple5) -> rule1))] Erin is quiet.[(triple5 OR ((triple6 triple4) -> rule3) OR ((triple6 ((triple1) -> rule4)) -> rule3))] Erin is red.[(triple6)] Erin is white.[(triple7 OR ((triple1) -> rule2) OR ((triple1 triple3) -> rule5))]
Erin is big.
("Erin" "is" "big" "+")
triple1
Erin is furry.
("Erin" "is" "furry" "+")
triple2
Erin is green.
("Erin" "is" "green" "+")
triple3
((triple4 triple7) -> (rule6 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
((triple4 ((triple1) -> (rule2 % int2))) -> (rule6 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
((((triple1) -> (rule4 % int2)) triple7) -> (rule6 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
((((triple1 triple5) -> (rule1 % int2)) triple7) -> (rule6 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
((((triple1) -> (rule4 % int3)) ((triple1) -> (rule2 % int2))) -> (rule6 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
((((triple1 triple5) -> (rule1 % int3)) ((triple1) -> (rule2 % int2))) -> (rule6 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Erin is kind.
("Erin" "is" "kind" "+")
triple4
((triple1) -> (rule4 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
((triple1 triple5) -> (rule1 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
triple5
((triple6 triple4) -> (rule3 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
((triple6 ((triple1) -> (rule4 % int2))) -> (rule3 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
triple6
Erin is white.
("Erin" "is" "white" "+")
triple7
((triple1) -> (rule2 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
((triple1 triple3) -> (rule5 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1