Erin is big. Erin is red. Erin is not round. All green things are big. If something is big then it is quiet. Red, green things are round. All rough, quiet things are blue. If something is quiet and not round then it is rough. If something is blue and not big then it is rough.
Erin is big.
("Erin" "is" "big" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is not round.
("Erin" "is" "round" "-")
All green things are big.
((("something" "is" "green" "+")) -> ("something" "is" "big" "+"))
If something is big then it is quiet.
((("something" "is" "big" "+")) -> ("something" "is" "quiet" "+"))
Red, green things are round.
((("something" "is" "red" "+") ("something" "is" "green" "+")) -> ("something" "is" "round" "+"))
All rough, quiet things are blue.
((("something" "is" "rough" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "blue" "+"))
If something is quiet and not round then it is rough.
((("something" "is" "quiet" "+") ("something" "is" "round" "~")) -> ("something" "is" "rough" "+"))
If something is blue and not big then it is rough.
((("something" "is" "blue" "+") ("something" "is" "big" "~")) -> ("something" "is" "rough" "+"))
Erin is red.
True
1
proof
[(triple2)]
("Erin" "is" "red" "+")
triple2
Erin is not big.
False
1
inv-proof
[(triple1)]
("Erin" "is" "big" "-")
triple1
Erin is quiet.
True
2
proof
[(((triple1) -> rule2))]
("Erin" "is" "quiet" "+")
((triple1) -> (rule2 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is not quiet.
False
2
inv-proof
[(((triple1) -> rule2))]
("Erin" "is" "quiet" "-")
((triple1) -> (rule2 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is rough.
True
4
proof
[(((((triple1) -> rule2) triple3) -> rule5))]
("Erin" "is" "rough" "+")
((((triple1) -> (rule2 % int2)) triple3) -> (rule5 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is not rough.
False
4
inv-proof
[(((((triple1) -> rule2) triple3) -> rule5))]
("Erin" "is" "rough" "-")
((((triple1) -> (rule2 % int2)) triple3) -> (rule5 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
@0: Erin is big.[(triple1)] Erin is not round.[(triple3)] Erin is red.[(triple2)] @1: Erin is quiet.[(((triple1) -> rule2))] @2: Erin is rough.[(((((triple1) -> rule2) triple3) -> rule5))] @3: Erin is blue.[(((((((triple1) -> rule2) triple3) -> rule5) ((triple1) -> rule2)) -> rule4))]
Erin is big.
("Erin" "is" "big" "+")
triple1
Erin is not round.
("Erin" "is" "round" "-")
triple3
Erin is red.
("Erin" "is" "red" "+")
triple2
Erin is quiet.
("Erin" "is" "quiet" "+")
((triple1) -> (rule2 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
((((triple1) -> (rule2 % int2)) triple3) -> (rule5 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
((((((triple1) -> (rule2 % int3)) triple3) -> (rule5 % int2)) ((triple1) -> (rule2 % int3))) -> (rule4 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
int3