Erin is red. Erin is not rough. Erin is white. Red things are young. Big things are young. If something is young and not rough then it is big. If something is white then it is big. If Erin is white and Erin is big then Erin is green. All green things are red. All young, green things are quiet. If something is rough and not big then it is quiet.
Erin is red.
("Erin" "is" "red" "+")
Erin is not rough.
("Erin" "is" "rough" "-")
Erin is white.
("Erin" "is" "white" "+")
Red things are young.
((("something" "is" "red" "+")) -> ("something" "is" "young" "+"))
Big things are young.
((("something" "is" "big" "+")) -> ("something" "is" "young" "+"))
If something is young and not rough then it is big.
((("something" "is" "young" "+") ("something" "is" "rough" "~")) -> ("something" "is" "big" "+"))
If something is white then it is big.
((("something" "is" "white" "+")) -> ("something" "is" "big" "+"))
If Erin is white and Erin is big then Erin is green.
((("Erin" "is" "white" "+") ("Erin" "is" "big" "+")) -> ("Erin" "is" "green" "+"))
All green things are red.
((("something" "is" "green" "+")) -> ("something" "is" "red" "+"))
All young, green things are quiet.
((("something" "is" "young" "+") ("something" "is" "green" "+")) -> ("something" "is" "quiet" "+"))
If something is rough and not big then it is quiet.
((("something" "is" "rough" "+") ("something" "is" "big" "~")) -> ("something" "is" "quiet" "+"))
Erin is white.
True
1
proof
[(triple3)]
("Erin" "is" "white" "+")
triple3
Erin is not red.
False
1
inv-proof
[(triple1 OR ((((triple3 ((triple3) -> rule4)) -> rule5)) -> rule6))]
("Erin" "is" "red" "-")
triple1
((((triple3 ((triple3) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3
Erin is big.
True
2
proof
[(((triple3) -> rule4) OR ((((triple1) -> rule1) triple2) -> rule3))]
("Erin" "is" "big" "+")
((triple3) -> (rule4 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
((((triple1) -> (rule1 % int2)) triple2) -> (rule3 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is not young.
False
2
inv-proof
[(((triple1) -> rule1) OR ((((triple3) -> rule4)) -> rule2) OR ((((((triple3 ((triple3) -> rule4)) -> rule5)) -> rule6)) -> rule1))]
("Erin" "is" "young" "-")
((triple1) -> (rule1 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
((((triple3) -> (rule4 % int2))) -> (rule2 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
((((((triple3 ((triple3) -> (rule4 % int4))) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
Erin is big.
("Erin" "is" "big" "+")
int4
Erin is green.
True
4
proof
[(((triple3 ((triple3) -> rule4)) -> rule5) OR ((triple3 ((((triple1) -> rule1) triple2) -> rule3)) -> rule5))]
("Erin" "is" "green" "+")
((triple3 ((triple3) -> (rule4 % int2))) -> (rule5 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
((triple3 ((((triple1) -> (rule1 % int3)) triple2) -> (rule3 % int2))) -> (rule5 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
Erin is not green.
False
4
inv-proof
[(((triple3 ((triple3) -> rule4)) -> rule5) OR ((triple3 ((((triple1) -> rule1) triple2) -> rule3)) -> rule5))]
("Erin" "is" "green" "-")
((triple3 ((triple3) -> (rule4 % int2))) -> (rule5 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
((triple3 ((((triple1) -> (rule1 % int3)) triple2) -> (rule3 % int2))) -> (rule5 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
Erin is quiet.
True
7
proof
[(((((triple1) -> rule1) ((triple3 ((triple3) -> rule4)) -> rule5)) -> rule7) OR ((((((triple3) -> rule4)) -> rule2) ((triple3 ((triple3) -> rule4)) -> rule5)) -> rule7) OR ((((triple1) -> rule1) ((triple3 ((((triple1) -> rule1) triple2) -> rule3)) -> rule5)) -> rule7) OR ((((((triple3) -> rule4)) -> rule2) ((triple3 ((((triple1) -> rule1) triple2) -> rule3)) -> rule5)) -> rule7) OR ((((((((triple3 ((triple3) -> rule4)) -> rule5)) -> rule6)) -> rule1) ((triple3 ((triple3) -> rule4)) -> rule5)) -> rule7) OR ((((((((triple3 ((triple3) -> rule4)) -> rule5)) -> rule6)) -> rule1) ((triple3 ((((triple1) -> rule1) triple2) -> rule3)) -> rule5)) -> rule7))]
("Erin" "is" "quiet" "+")
((((triple1) -> (rule1 % int4)) ((triple3 ((triple3) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3
Erin is young.
("Erin" "is" "young" "+")
int4
((((((triple3) -> (rule4 % int4))) -> (rule2 % int3)) ((triple3 ((triple3) -> (rule4 % int4))) -> (rule5 % int2))) -> (rule7 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
Erin is big.
("Erin" "is" "big" "+")
int4
((((triple1) -> (rule1 % int4)) ((triple3 ((((triple1) -> (rule1 % int4)) triple2) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3
Erin is young.
("Erin" "is" "young" "+")
int4
((((((triple3) -> (rule4 % int4))) -> (rule2 % int3)) ((triple3 ((((triple1) -> (rule1 % int3)) triple2) -> (rule3 % int4))) -> (rule5 % int2))) -> (rule7 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
Erin is big.
("Erin" "is" "big" "+")
int4
((((((((triple3 ((triple3) -> (rule4 % int5))) -> (rule5 % int4))) -> (rule6 % int3))) -> (rule1 % int2)) ((triple3 ((triple3) -> (rule4 % int5))) -> (rule5 % int4))) -> (rule7 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
Erin is green.
("Erin" "is" "green" "+")
int4
Erin is big.
("Erin" "is" "big" "+")
int5
((((((((triple3 ((triple3) -> (rule4 % int5))) -> (rule5 % int4))) -> (rule6 % int3))) -> (rule1 % int2)) ((triple3 ((((triple1) -> (rule1 % int2)) triple2) -> (rule3 % int5))) -> (rule5 % int4))) -> (rule7 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
Erin is green.
("Erin" "is" "green" "+")
int4
Erin is big.
("Erin" "is" "big" "+")
int5
Erin is not quiet.
False
7
inv-proof
[(((((triple1) -> rule1) ((triple3 ((triple3) -> rule4)) -> rule5)) -> rule7) OR ((((((triple3) -> rule4)) -> rule2) ((triple3 ((triple3) -> rule4)) -> rule5)) -> rule7) OR ((((triple1) -> rule1) ((triple3 ((((triple1) -> rule1) triple2) -> rule3)) -> rule5)) -> rule7) OR ((((((triple3) -> rule4)) -> rule2) ((triple3 ((((triple1) -> rule1) triple2) -> rule3)) -> rule5)) -> rule7) OR ((((((((triple3 ((triple3) -> rule4)) -> rule5)) -> rule6)) -> rule1) ((triple3 ((triple3) -> rule4)) -> rule5)) -> rule7) OR ((((((((triple3 ((triple3) -> rule4)) -> rule5)) -> rule6)) -> rule1) ((triple3 ((((triple1) -> rule1) triple2) -> rule3)) -> rule5)) -> rule7))]
("Erin" "is" "quiet" "-")
((((triple1) -> (rule1 % int4)) ((triple3 ((triple3) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3
Erin is young.
("Erin" "is" "young" "+")
int4
((((((triple3) -> (rule4 % int4))) -> (rule2 % int3)) ((triple3 ((triple3) -> (rule4 % int4))) -> (rule5 % int2))) -> (rule7 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
Erin is big.
("Erin" "is" "big" "+")
int4
((((triple1) -> (rule1 % int4)) ((triple3 ((((triple1) -> (rule1 % int4)) triple2) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3
Erin is young.
("Erin" "is" "young" "+")
int4
((((((triple3) -> (rule4 % int4))) -> (rule2 % int3)) ((triple3 ((((triple1) -> (rule1 % int3)) triple2) -> (rule3 % int4))) -> (rule5 % int2))) -> (rule7 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
Erin is big.
("Erin" "is" "big" "+")
int4
((((((((triple3 ((triple3) -> (rule4 % int5))) -> (rule5 % int4))) -> (rule6 % int3))) -> (rule1 % int2)) ((triple3 ((triple3) -> (rule4 % int5))) -> (rule5 % int4))) -> (rule7 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
Erin is green.
("Erin" "is" "green" "+")
int4
Erin is big.
("Erin" "is" "big" "+")
int5
((((((((triple3 ((triple3) -> (rule4 % int5))) -> (rule5 % int4))) -> (rule6 % int3))) -> (rule1 % int2)) ((triple3 ((((triple1) -> (rule1 % int2)) triple2) -> (rule3 % int5))) -> (rule5 % int4))) -> (rule7 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
Erin is green.
("Erin" "is" "green" "+")
int4
Erin is big.
("Erin" "is" "big" "+")
int5
@0: Erin is not rough.[(triple2)] Erin is red.[(triple1 OR ((((triple3 ((triple3) -> rule4)) -> rule5)) -> rule6))] Erin is white.[(triple3)] @1: Erin is big.[(((triple3) -> rule4) OR ((((triple1) -> rule1) triple2) -> rule3))] Erin is young.[(((triple1) -> rule1) OR ((((triple3) -> rule4)) -> rule2) OR ((((((triple3 ((triple3) -> rule4)) -> rule5)) -> rule6)) -> rule1))] @2: Erin is green.[(((triple3 ((triple3) -> rule4)) -> rule5) OR ((triple3 ((((triple1) -> rule1) triple2) -> rule3)) -> rule5))] @3: Erin is quiet.[(((((triple1) -> rule1) ((triple3 ((triple3) -> rule4)) -> rule5)) -> rule7) OR ((((((triple3) -> rule4)) -> rule2) ((triple3 ((triple3) -> rule4)) -> rule5)) -> rule7) OR ((((triple1) -> rule1) ((triple3 ((((triple1) -> rule1) triple2) -> rule3)) -> rule5)) -> rule7) OR ((((((triple3) -> rule4)) -> rule2) ((triple3 ((((triple1) -> rule1) triple2) -> rule3)) -> rule5)) -> rule7) OR ((((((((triple3 ((triple3) -> rule4)) -> rule5)) -> rule6)) -> rule1) ((triple3 ((triple3) -> rule4)) -> rule5)) -> rule7) OR ((((((((triple3 ((triple3) -> rule4)) -> rule5)) -> rule6)) -> rule1) ((triple3 ((((triple1) -> rule1) triple2) -> rule3)) -> rule5)) -> rule7))]
Erin is not rough.
("Erin" "is" "rough" "-")
triple2
Erin is red.
("Erin" "is" "red" "+")
triple1
((((triple3 ((triple3) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3
Erin is white.
("Erin" "is" "white" "+")
triple3
Erin is big.
("Erin" "is" "big" "+")
((triple3) -> (rule4 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
((((triple1) -> (rule1 % int2)) triple2) -> (rule3 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
((triple1) -> (rule1 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
((((triple3) -> (rule4 % int2))) -> (rule2 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
((((((triple3 ((triple3) -> (rule4 % int4))) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
Erin is big.
("Erin" "is" "big" "+")
int4
Erin is green.
("Erin" "is" "green" "+")
((triple3 ((triple3) -> (rule4 % int2))) -> (rule5 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
((triple3 ((((triple1) -> (rule1 % int3)) triple2) -> (rule3 % int2))) -> (rule5 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
Erin is quiet.
("Erin" "is" "quiet" "+")
((((triple1) -> (rule1 % int4)) ((triple3 ((triple3) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3
Erin is young.
("Erin" "is" "young" "+")
int4
((((((triple3) -> (rule4 % int4))) -> (rule2 % int3)) ((triple3 ((triple3) -> (rule4 % int4))) -> (rule5 % int2))) -> (rule7 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
Erin is big.
("Erin" "is" "big" "+")
int4
((((triple1) -> (rule1 % int4)) ((triple3 ((((triple1) -> (rule1 % int4)) triple2) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3
Erin is young.
("Erin" "is" "young" "+")
int4
((((((triple3) -> (rule4 % int4))) -> (rule2 % int3)) ((triple3 ((((triple1) -> (rule1 % int3)) triple2) -> (rule3 % int4))) -> (rule5 % int2))) -> (rule7 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
Erin is big.
("Erin" "is" "big" "+")
int4
((((((((triple3 ((triple3) -> (rule4 % int5))) -> (rule5 % int4))) -> (rule6 % int3))) -> (rule1 % int2)) ((triple3 ((triple3) -> (rule4 % int5))) -> (rule5 % int4))) -> (rule7 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
Erin is green.
("Erin" "is" "green" "+")
int4
Erin is big.
("Erin" "is" "big" "+")
int5
((((((((triple3 ((triple3) -> (rule4 % int5))) -> (rule5 % int4))) -> (rule6 % int3))) -> (rule1 % int2)) ((triple3 ((((triple1) -> (rule1 % int2)) triple2) -> (rule3 % int5))) -> (rule5 % int4))) -> (rule7 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
Erin is green.
("Erin" "is" "green" "+")
int4
Erin is big.
("Erin" "is" "big" "+")
int5