Erin is blue. Erin is cold. Erin is nice. Erin is red. Erin is rough. Erin is smart. Erin is white. If Erin is blue and Erin is smart then Erin is white. If something is rough and white then it is cold. If Erin is red and Erin is nice then Erin is blue.
Erin is blue.
("Erin" "is" "blue" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Erin is white.
("Erin" "is" "white" "+")
If Erin is blue and Erin is smart then Erin is white.
((("Erin" "is" "blue" "+") ("Erin" "is" "smart" "+")) -> ("Erin" "is" "white" "+"))
If something is rough and white then it is cold.
((("something" "is" "rough" "+") ("something" "is" "white" "+")) -> ("something" "is" "cold" "+"))
If Erin is red and Erin is nice then Erin is blue.
((("Erin" "is" "red" "+") ("Erin" "is" "nice" "+")) -> ("Erin" "is" "blue" "+"))
Erin is smart.
True
1
proof
[(triple6)]
("Erin" "is" "smart" "+")
triple6
Erin is not white.
False
1
inv-proof
[(triple7 OR ((triple1 triple6) -> rule1) OR ((((triple4 triple3) -> rule3) triple6) -> rule1))]
("Erin" "is" "white" "-")
triple7
((triple1 triple6) -> (rule1 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
((((triple4 triple3) -> (rule3 % int2)) triple6) -> (rule1 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
@0: Erin is blue.[(triple1 OR ((triple4 triple3) -> rule3))] Erin is cold.[(triple2 OR ((triple5 triple7) -> rule2) OR ((triple5 ((triple1 triple6) -> rule1)) -> rule2) OR ((triple5 ((((triple4 triple3) -> rule3) triple6) -> rule1)) -> rule2))] Erin is nice.[(triple3)] Erin is red.[(triple4)] Erin is rough.[(triple5)] Erin is smart.[(triple6)] Erin is white.[(triple7 OR ((triple1 triple6) -> rule1) OR ((((triple4 triple3) -> rule3) triple6) -> rule1))]
Erin is blue.
("Erin" "is" "blue" "+")
triple1
((triple4 triple3) -> (rule3 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
triple2
((triple5 triple7) -> (rule2 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
((triple5 ((triple1 triple6) -> (rule1 % int2))) -> (rule2 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
((triple5 ((((triple4 triple3) -> (rule3 % int3)) triple6) -> (rule1 % int2))) -> (rule2 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3
Erin is nice.
("Erin" "is" "nice" "+")
triple3
Erin is red.
("Erin" "is" "red" "+")
triple4
Erin is rough.
("Erin" "is" "rough" "+")
triple5
Erin is smart.
("Erin" "is" "smart" "+")
triple6
Erin is white.
("Erin" "is" "white" "+")
triple7
((triple1 triple6) -> (rule1 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
((((triple4 triple3) -> (rule3 % int2)) triple6) -> (rule1 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2