Erin is big. Erin is cold. Erin is green. Erin is nice. Erin is rough. Erin is not round. Erin is smart. Gary is big. Gary is cold. Gary is green. Gary is not nice. Gary is rough. Gary is round. Gary is smart. All nice, cold people are smart. Round people are green. If someone is smart and nice then they are green. If Gary is rough and Gary is big then Gary is cold. If Gary is round then Gary is rough. If someone is smart and not round then they are big. If Erin is round then Erin is cold. If someone is big and green then they are cold.
Erin is big.
("Erin" "is" "big" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is not round.
("Erin" "is" "round" "-")
Erin is smart.
("Erin" "is" "smart" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is not nice.
("Gary" "is" "nice" "-")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is round.
("Gary" "is" "round" "+")
Gary is smart.
("Gary" "is" "smart" "+")
All nice, cold people are smart.
((("someone" "is" "nice" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "smart" "+"))
Round people are green.
((("someone" "is" "round" "+")) -> ("someone" "is" "green" "+"))
If someone is smart and nice then they are green.
((("someone" "is" "smart" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "green" "+"))
If Gary is rough and Gary is big then Gary is cold.
((("Gary" "is" "rough" "+") ("Gary" "is" "big" "+")) -> ("Gary" "is" "cold" "+"))
If Gary is round then Gary is rough.
((("Gary" "is" "round" "+")) -> ("Gary" "is" "rough" "+"))
If someone is smart and not round then they are big.
((("someone" "is" "smart" "+") ("someone" "is" "round" "~")) -> ("someone" "is" "big" "+"))
If Erin is round then Erin is cold.
((("Erin" "is" "round" "+")) -> ("Erin" "is" "cold" "+"))
If someone is big and green then they are cold.
((("someone" "is" "big" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "cold" "+"))
Gary is green.
True
1
proof
[(triple10 OR ((triple13) -> rule2))]
("Gary" "is" "green" "+")
triple10
((triple13) -> (rule2 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is not green.
False
1
inv-proof
[(triple10 OR ((triple13) -> rule2))]
("Gary" "is" "green" "-")
triple10
((triple13) -> (rule2 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
@0: Erin is big.[(triple1 OR ((triple7 triple6) -> rule6) OR ((((triple4 triple2) -> rule1) triple6) -> rule6))] Erin is cold.[(triple2 OR ((triple1 triple3) -> rule8) OR ((triple1 ((triple7 triple4) -> rule3)) -> rule8) OR ((((triple7 triple6) -> rule6) triple3) -> rule8) OR ((((triple7 triple6) -> rule6) ((triple7 triple4) -> rule3)) -> rule8))] Erin is green.[(triple3 OR ((triple7 triple4) -> rule3) OR ((((triple4 triple2) -> rule1) triple4) -> rule3))] Erin is nice.[(triple4)] Erin is not round.[(triple6)] Erin is rough.[(triple5)] Erin is smart.[(triple7 OR ((triple4 triple2) -> rule1) OR ((triple4 ((triple1 triple3) -> rule8)) -> rule1))] Gary is big.[(triple8)] Gary is cold.[(triple9 OR ((triple12 triple8) -> rule4) OR ((triple8 triple10) -> rule8) OR ((triple8 ((triple13) -> rule2)) -> rule8) OR ((((triple13) -> rule5) triple8) -> rule4))] Gary is green.[(triple10 OR ((triple13) -> rule2))] Gary is not nice.[(triple11)] Gary is rough.[(triple12 OR ((triple13) -> rule5))] Gary is round.[(triple13)] Gary is smart.[(triple14)]
Erin is big.
("Erin" "is" "big" "+")
triple1
((triple7 triple6) -> (rule6 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
((((triple4 triple2) -> (rule1 % int2)) triple6) -> (rule6 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
triple2
((triple1 triple3) -> (rule8 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
((triple1 ((triple7 triple4) -> (rule3 % int2))) -> (rule8 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
((((triple7 triple6) -> (rule6 % int2)) triple3) -> (rule8 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
((((triple7 triple6) -> (rule6 % int3)) ((triple7 triple4) -> (rule3 % int2))) -> (rule8 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3
Erin is green.
("Erin" "is" "green" "+")
triple3
((triple7 triple4) -> (rule3 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
((((triple4 triple2) -> (rule1 % int2)) triple4) -> (rule3 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
triple4
Erin is not round.
("Erin" "is" "round" "-")
triple6
Erin is rough.
("Erin" "is" "rough" "+")
triple5
Erin is smart.
("Erin" "is" "smart" "+")
triple7
((triple4 triple2) -> (rule1 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
((triple4 ((triple1 triple3) -> (rule8 % int2))) -> (rule1 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
triple8
Gary is cold.
("Gary" "is" "cold" "+")
triple9
((triple12 triple8) -> (rule4 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
((triple8 triple10) -> (rule8 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
((triple8 ((triple13) -> (rule2 % int2))) -> (rule8 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
((((triple13) -> (rule5 % int2)) triple8) -> (rule4 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
triple10
((triple13) -> (rule2 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is not nice.
("Gary" "is" "nice" "-")
triple11
Gary is rough.
("Gary" "is" "rough" "+")
triple12
((triple13) -> (rule5 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
triple13
Gary is smart.
("Gary" "is" "smart" "+")
triple14