Erin is blue. Erin is smart. Erin is white. If something is smart then it is round. If something is big then it is white. If Erin is white then Erin is big. Smart, big things are rough. If something is round and not white then it is blue. If Erin is furry and Erin is not rough then Erin is round.
Erin is blue.
("Erin" "is" "blue" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Erin is white.
("Erin" "is" "white" "+")
If something is smart then it is round.
((("something" "is" "smart" "+")) -> ("something" "is" "round" "+"))
If something is big then it is white.
((("something" "is" "big" "+")) -> ("something" "is" "white" "+"))
If Erin is white then Erin is big.
((("Erin" "is" "white" "+")) -> ("Erin" "is" "big" "+"))
Smart, big things are rough.
((("something" "is" "smart" "+") ("something" "is" "big" "+")) -> ("something" "is" "rough" "+"))
If something is round and not white then it is blue.
((("something" "is" "round" "+") ("something" "is" "white" "~")) -> ("something" "is" "blue" "+"))
If Erin is furry and Erin is not rough then Erin is round.
((("Erin" "is" "furry" "+") ("Erin" "is" "rough" "~")) -> ("Erin" "is" "round" "+"))
Erin is smart.
True
1
proof
[(triple2)]
("Erin" "is" "smart" "+")
triple2
Erin is not white.
False
1
inv-proof
[(triple3)]
("Erin" "is" "white" "-")
triple3
Erin is big.
True
2
proof
[(((triple3) -> rule3))]
("Erin" "is" "big" "+")
((triple3) -> (rule3 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is not round.
False
2
inv-proof
[(((triple2) -> rule1))]
("Erin" "is" "round" "-")
((triple2) -> (rule1 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is rough.
True
4
proof
[(((triple2 ((triple3) -> rule3)) -> rule4))]
("Erin" "is" "rough" "+")
((triple2 ((triple3) -> (rule3 % int2))) -> (rule4 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is not rough.
False
4
inv-proof
[(((triple2 ((triple3) -> rule3)) -> rule4))]
("Erin" "is" "rough" "-")
((triple2 ((triple3) -> (rule3 % int2))) -> (rule4 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
@0: Erin is blue.[(triple1)] Erin is smart.[(triple2)] Erin is white.[(triple3)] @1: Erin is big.[(((triple3) -> rule3))] Erin is round.[(((triple2) -> rule1))] @2: Erin is rough.[(((triple2 ((triple3) -> rule3)) -> rule4))]
Erin is blue.
("Erin" "is" "blue" "+")
triple1
Erin is smart.
("Erin" "is" "smart" "+")
triple2
Erin is white.
("Erin" "is" "white" "+")
triple3
Erin is big.
("Erin" "is" "big" "+")
((triple3) -> (rule3 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
((triple2) -> (rule1 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
((triple2 ((triple3) -> (rule3 % int2))) -> (rule4 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2