Erin is not big. Erin is cold. Erin is green. Erin is quiet. Erin is round. Erin is smart. Erin is white. White, round people are smart. If someone is round and big then they are not smart. All round, green people are smart. Cold people are round. All round people are white. Smart, quiet people are not big.
Erin is not big.
("Erin" "is" "big" "-")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is round.
("Erin" "is" "round" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Erin is white.
("Erin" "is" "white" "+")
White, round people are smart.
((("someone" "is" "white" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "smart" "+"))
If someone is round and big then they are not smart.
((("someone" "is" "round" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "smart" "-"))
All round, green people are smart.
((("someone" "is" "round" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "smart" "+"))
Cold people are round.
((("someone" "is" "cold" "+")) -> ("someone" "is" "round" "+"))
All round people are white.
((("someone" "is" "round" "+")) -> ("someone" "is" "white" "+"))
Smart, quiet people are not big.
((("someone" "is" "smart" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "big" "-"))
Erin is smart.
True
1
proof
[(triple6 OR ((triple5 triple3) -> rule3) OR ((triple7 triple5) -> rule1) OR ((triple7 ((triple2) -> rule4)) -> rule1) OR ((((triple2) -> rule4) triple3) -> rule3) OR ((((triple5) -> rule5) triple5) -> rule1) OR ((((triple5) -> rule5) ((triple2) -> rule4)) -> rule1) OR ((((((triple2) -> rule4)) -> rule5) triple5) -> rule1) OR ((((((triple2) -> rule4)) -> rule5) ((triple2) -> rule4)) -> rule1))]
("Erin" "is" "smart" "+")
triple6
((triple5 triple3) -> (rule3 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
((triple7 triple5) -> (rule1 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
((triple7 ((triple2) -> (rule4 % int2))) -> (rule1 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
((((triple2) -> (rule4 % int2)) triple3) -> (rule3 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
((((triple5) -> (rule5 % int2)) triple5) -> (rule1 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
((((triple5) -> (rule5 % int3)) ((triple2) -> (rule4 % int2))) -> (rule1 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
int3
((((((triple2) -> (rule4 % int3))) -> (rule5 % int2)) triple5) -> (rule1 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
((((((triple2) -> (rule4 % int3))) -> (rule5 % int2)) ((triple2) -> (rule4 % int3))) -> (rule1 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
Erin is not green.
False
1
inv-proof
[(triple3)]
("Erin" "is" "green" "-")
triple3
@0: Erin is cold.[(triple2)] Erin is green.[(triple3)] Erin is not big.[(triple1 OR ((triple6 triple4) -> rule6) OR ((((triple5 triple3) -> rule3) triple4) -> rule6) OR ((((triple7 triple5) -> rule1) triple4) -> rule6) OR ((((triple7 ((triple2) -> rule4)) -> rule1) triple4) -> rule6) OR ((((((triple2) -> rule4) triple3) -> rule3) triple4) -> rule6) OR ((((((triple5) -> rule5) triple5) -> rule1) triple4) -> rule6) OR ((((((triple5) -> rule5) ((triple2) -> rule4)) -> rule1) triple4) -> rule6) OR ((((((((triple2) -> rule4)) -> rule5) triple5) -> rule1) triple4) -> rule6) OR ((((((((triple2) -> rule4)) -> rule5) ((triple2) -> rule4)) -> rule1) triple4) -> rule6))] Erin is quiet.[(triple4)] Erin is round.[(triple5 OR ((triple2) -> rule4))] Erin is smart.[(triple6 OR ((triple5 triple3) -> rule3) OR ((triple7 triple5) -> rule1) OR ((triple7 ((triple2) -> rule4)) -> rule1) OR ((((triple2) -> rule4) triple3) -> rule3) OR ((((triple5) -> rule5) triple5) -> rule1) OR ((((triple5) -> rule5) ((triple2) -> rule4)) -> rule1) OR ((((((triple2) -> rule4)) -> rule5) triple5) -> rule1) OR ((((((triple2) -> rule4)) -> rule5) ((triple2) -> rule4)) -> rule1))] Erin is white.[(triple7 OR ((triple5) -> rule5) OR ((((triple2) -> rule4)) -> rule5))]
Erin is cold.
("Erin" "is" "cold" "+")
triple2
Erin is green.
("Erin" "is" "green" "+")
triple3
Erin is not big.
("Erin" "is" "big" "-")
triple1
((triple6 triple4) -> (rule6 % int1))
Erin is not big.
("Erin" "is" "big" "-")
int1
((((triple5 triple3) -> (rule3 % int2)) triple4) -> (rule6 % int1))
Erin is not big.
("Erin" "is" "big" "-")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
((((triple7 triple5) -> (rule1 % int2)) triple4) -> (rule6 % int1))
Erin is not big.
("Erin" "is" "big" "-")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
((((triple7 ((triple2) -> (rule4 % int3))) -> (rule1 % int2)) triple4) -> (rule6 % int1))
Erin is not big.
("Erin" "is" "big" "-")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
((((((triple2) -> (rule4 % int3)) triple3) -> (rule3 % int2)) triple4) -> (rule6 % int1))
Erin is not big.
("Erin" "is" "big" "-")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
((((((triple5) -> (rule5 % int3)) triple5) -> (rule1 % int2)) triple4) -> (rule6 % int1))
Erin is not big.
("Erin" "is" "big" "-")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
int3
((((((triple5) -> (rule5 % int4)) ((triple2) -> (rule4 % int3))) -> (rule1 % int2)) triple4) -> (rule6 % int1))
Erin is not big.
("Erin" "is" "big" "-")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
Erin is white.
("Erin" "is" "white" "+")
int4
((((((((triple2) -> (rule4 % int4))) -> (rule5 % int3)) triple5) -> (rule1 % int2)) triple4) -> (rule6 % int1))
Erin is not big.
("Erin" "is" "big" "-")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
int3
Erin is round.
("Erin" "is" "round" "+")
int4
((((((((triple2) -> (rule4 % int4))) -> (rule5 % int3)) ((triple2) -> (rule4 % int4))) -> (rule1 % int2)) triple4) -> (rule6 % int1))
Erin is not big.
("Erin" "is" "big" "-")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
int3
Erin is round.
("Erin" "is" "round" "+")
int4
Erin is quiet.
("Erin" "is" "quiet" "+")
triple4
Erin is round.
("Erin" "is" "round" "+")
triple5
((triple2) -> (rule4 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
triple6
((triple5 triple3) -> (rule3 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
((triple7 triple5) -> (rule1 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
((triple7 ((triple2) -> (rule4 % int2))) -> (rule1 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
((((triple2) -> (rule4 % int2)) triple3) -> (rule3 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
((((triple5) -> (rule5 % int2)) triple5) -> (rule1 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
((((triple5) -> (rule5 % int3)) ((triple2) -> (rule4 % int2))) -> (rule1 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
int3
((((((triple2) -> (rule4 % int3))) -> (rule5 % int2)) triple5) -> (rule1 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
((((((triple2) -> (rule4 % int3))) -> (rule5 % int2)) ((triple2) -> (rule4 % int3))) -> (rule1 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
Erin is white.
("Erin" "is" "white" "+")
triple7
((triple5) -> (rule5 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
((((triple2) -> (rule4 % int2))) -> (rule5 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2