Erin is big. Erin is blue. Erin is furry. Erin is kind. Erin is round. Erin is white. Gary is big. Gary is blue. Gary is furry. Gary is green. Gary is kind. Gary is round. If something is white and blue then it is not green. If something is white and furry then it is big. If Gary is big then Gary is kind. If Erin is blue then Erin is kind. If Gary is green then Gary is blue. Green things are kind. If something is kind and not big then it is round. All white things are round.
Erin is big.
("Erin" "is" "big" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is round.
("Erin" "is" "round" "+")
Erin is white.
("Erin" "is" "white" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is round.
("Gary" "is" "round" "+")
If something is white and blue then it is not green.
((("something" "is" "white" "+") ("something" "is" "blue" "+")) -> ("something" "is" "green" "-"))
If something is white and furry then it is big.
((("something" "is" "white" "+") ("something" "is" "furry" "+")) -> ("something" "is" "big" "+"))
If Gary is big then Gary is kind.
((("Gary" "is" "big" "+")) -> ("Gary" "is" "kind" "+"))
If Erin is blue then Erin is kind.
((("Erin" "is" "blue" "+")) -> ("Erin" "is" "kind" "+"))
If Gary is green then Gary is blue.
((("Gary" "is" "green" "+")) -> ("Gary" "is" "blue" "+"))
Green things are kind.
((("something" "is" "green" "+")) -> ("something" "is" "kind" "+"))
If something is kind and not big then it is round.
((("something" "is" "kind" "+") ("something" "is" "big" "~")) -> ("something" "is" "round" "+"))
All white things are round.
((("something" "is" "white" "+")) -> ("something" "is" "round" "+"))
Gary is blue.
True
1
proof
[(triple8 OR ((triple10) -> rule5))]
("Gary" "is" "blue" "+")
triple8
((triple10) -> (rule5 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is not blue.
False
1
inv-proof
[(triple8 OR ((triple10) -> rule5))]
("Gary" "is" "blue" "-")
triple8
((triple10) -> (rule5 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Erin is not green.
True
3
proof
[(((triple6 triple2) -> rule1))]
("Erin" "is" "green" "-")
((triple6 triple2) -> (rule1 % int1))
Erin is not green.
("Erin" "is" "green" "-")
int1
Erin is green.
False
3
inv-proof
[(((triple6 triple2) -> rule1))]
("Erin" "is" "green" "+")
((triple6 triple2) -> (rule1 % int1))
Erin is not green.
("Erin" "is" "green" "-")
int1
@0: Erin is big.[(triple1 OR ((triple6 triple3) -> rule2))] Erin is blue.[(triple2)] Erin is furry.[(triple3)] Erin is kind.[(triple4 OR ((triple2) -> rule4))] Erin is round.[(triple5 OR ((triple6) -> rule8))] Erin is white.[(triple6)] Gary is big.[(triple7)] Gary is blue.[(triple8 OR ((triple10) -> rule5))] Gary is furry.[(triple9)] Gary is green.[(triple10)] Gary is kind.[(triple11 OR ((triple10) -> rule6) OR ((triple7) -> rule3))] Gary is round.[(triple12)] @1: Erin is not green.[(((triple6 triple2) -> rule1))]
Erin is big.
("Erin" "is" "big" "+")
triple1
((triple6 triple3) -> (rule2 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
triple2
Erin is furry.
("Erin" "is" "furry" "+")
triple3
Erin is kind.
("Erin" "is" "kind" "+")
triple4
((triple2) -> (rule4 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
triple5
((triple6) -> (rule8 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
triple6
Gary is big.
("Gary" "is" "big" "+")
triple7
Gary is blue.
("Gary" "is" "blue" "+")
triple8
((triple10) -> (rule5 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
triple9
Gary is green.
("Gary" "is" "green" "+")
triple10
Gary is kind.
("Gary" "is" "kind" "+")
triple11
((triple10) -> (rule6 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
((triple7) -> (rule3 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
triple12
Erin is not green.
("Erin" "is" "green" "-")
((triple6 triple2) -> (rule1 % int1))
Erin is not green.
("Erin" "is" "green" "-")
int1