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