Anne is kind. Anne is quiet. Anne is round. Erin is big. Erin is kind. Erin is nice. Erin is quiet. Erin is round. Gary is big. Gary is green. Gary is kind. Gary is nice. Gary is quiet. Gary is red. Gary is round. If Erin is quiet then Erin is nice. Kind, red things are green. If something is nice then it is red. All green, kind things are big. All red things are nice. If something is kind then it is nice.
Anne is kind.
("Anne" "is" "kind" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is round.
("Anne" "is" "round" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is round.
("Erin" "is" "round" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is round.
("Gary" "is" "round" "+")
If Erin is quiet then Erin is nice.
((("Erin" "is" "quiet" "+")) -> ("Erin" "is" "nice" "+"))
Kind, red things are green.
((("something" "is" "kind" "+") ("something" "is" "red" "+")) -> ("something" "is" "green" "+"))
If something is nice then it is red.
((("something" "is" "nice" "+")) -> ("something" "is" "red" "+"))
All green, kind things are big.
((("something" "is" "green" "+") ("something" "is" "kind" "+")) -> ("something" "is" "big" "+"))
All red things are nice.
((("something" "is" "red" "+")) -> ("something" "is" "nice" "+"))
If something is kind then it is nice.
((("something" "is" "kind" "+")) -> ("something" "is" "nice" "+"))
Erin is nice.
True
1
proof
[(triple6 OR ((triple5) -> rule6) OR ((triple7) -> rule1))]
("Erin" "is" "nice" "+")
triple6
((triple5) -> (rule6 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
((triple7) -> (rule1 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is not round.
False
1
inv-proof
[(triple8)]
("Erin" "is" "round" "-")
triple8
Anne is nice.
True
2
proof
[(((triple1) -> rule6))]
("Anne" "is" "nice" "+")
((triple1) -> (rule6 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Erin is not red.
False
2
inv-proof
[(((triple6) -> rule3) OR ((((triple5) -> rule6)) -> rule3) OR ((((triple7) -> rule1)) -> rule3))]
("Erin" "is" "red" "-")
((triple6) -> (rule3 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
((((triple5) -> (rule6 % int2))) -> (rule3 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
((((triple7) -> (rule1 % int2))) -> (rule3 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is green.
True
4
proof
[(((triple5 ((triple6) -> rule3)) -> rule2) OR ((triple5 ((((triple5) -> rule6)) -> rule3)) -> rule2) OR ((triple5 ((((triple7) -> rule1)) -> rule3)) -> rule2))]
("Erin" "is" "green" "+")
((triple5 ((triple6) -> (rule3 % int2))) -> (rule2 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
((triple5 ((((triple5) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
int3
((triple5 ((((triple7) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
int3
Anne is not red.
False
3
inv-proof
[(((((triple1) -> rule6)) -> rule3))]
("Anne" "is" "red" "-")
((((triple1) -> (rule6 % int2))) -> (rule3 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is green.
True
5
proof
[(((triple1 ((((triple1) -> rule6)) -> rule3)) -> rule2))]
("Anne" "is" "green" "+")
((triple1 ((((triple1) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
Anne is not green.
False
5
inv-proof
[(((triple1 ((((triple1) -> rule6)) -> rule3)) -> rule2))]
("Anne" "is" "green" "-")
((triple1 ((((triple1) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
@0: Anne is kind.[(triple1)] Anne is quiet.[(triple2)] Anne is round.[(triple3)] Erin is big.[(triple4 OR ((((triple5 ((triple6) -> rule3)) -> rule2) triple5) -> rule4) OR ((((triple5 ((((triple5) -> rule6)) -> rule3)) -> rule2) triple5) -> rule4) OR ((((triple5 ((((triple7) -> rule1)) -> rule3)) -> rule2) triple5) -> rule4))] Erin is kind.[(triple5)] Erin is nice.[(triple6 OR ((triple5) -> rule6) OR ((triple7) -> rule1))] Erin is quiet.[(triple7)] Erin is round.[(triple8)] Gary is big.[(triple9 OR ((triple10 triple11) -> rule4) OR ((((triple11 triple14) -> rule2) triple11) -> rule4) OR ((((triple11 ((triple12) -> rule3)) -> rule2) triple11) -> rule4) OR ((((triple11 ((((triple11) -> rule6)) -> rule3)) -> rule2) triple11) -> rule4))] Gary is green.[(triple10 OR ((triple11 triple14) -> rule2) OR ((triple11 ((triple12) -> rule3)) -> rule2) OR ((triple11 ((((triple11) -> rule6)) -> rule3)) -> rule2))] Gary is kind.[(triple11)] Gary is nice.[(triple12 OR ((triple11) -> rule6) OR ((triple14) -> rule5))] Gary is quiet.[(triple13)] Gary is red.[(triple14 OR ((triple12) -> rule3) OR ((((triple11) -> rule6)) -> rule3))] Gary is round.[(triple15)] @1: Anne is nice.[(((triple1) -> rule6))] Erin is red.[(((triple6) -> rule3) OR ((((triple5) -> rule6)) -> rule3) OR ((((triple7) -> rule1)) -> rule3))] @2: Anne is red.[(((((triple1) -> rule6)) -> rule3))] Erin is green.[(((triple5 ((triple6) -> rule3)) -> rule2) OR ((triple5 ((((triple5) -> rule6)) -> rule3)) -> rule2) OR ((triple5 ((((triple7) -> rule1)) -> rule3)) -> rule2))] @3: Anne is green.[(((triple1 ((((triple1) -> rule6)) -> rule3)) -> rule2))] @4: Anne is big.[(((((triple1 ((((triple1) -> rule6)) -> rule3)) -> rule2) triple1) -> rule4))]
Anne is kind.
("Anne" "is" "kind" "+")
triple1
Anne is quiet.
("Anne" "is" "quiet" "+")
triple2
Anne is round.
("Anne" "is" "round" "+")
triple3
Erin is big.
("Erin" "is" "big" "+")
triple4
((((triple5 ((triple6) -> (rule3 % int3))) -> (rule2 % int2)) triple5) -> (rule4 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
((((triple5 ((((triple5) -> (rule6 % int4))) -> (rule3 % int3))) -> (rule2 % int2)) triple5) -> (rule4 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
Erin is nice.
("Erin" "is" "nice" "+")
int4
((((triple5 ((((triple7) -> (rule1 % int4))) -> (rule3 % int3))) -> (rule2 % int2)) triple5) -> (rule4 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
Erin is nice.
("Erin" "is" "nice" "+")
int4
Erin is kind.
("Erin" "is" "kind" "+")
triple5
Erin is nice.
("Erin" "is" "nice" "+")
triple6
((triple5) -> (rule6 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
((triple7) -> (rule1 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
triple7
Erin is round.
("Erin" "is" "round" "+")
triple8
Gary is big.
("Gary" "is" "big" "+")
triple9
((triple10 triple11) -> (rule4 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
((((triple11 triple14) -> (rule2 % int2)) triple11) -> (rule4 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
((((triple11 ((triple12) -> (rule3 % int3))) -> (rule2 % int2)) triple11) -> (rule4 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
((((triple11 ((((triple11) -> (rule6 % int4))) -> (rule3 % int3))) -> (rule2 % int2)) triple11) -> (rule4 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
Gary is nice.
("Gary" "is" "nice" "+")
int4
Gary is green.
("Gary" "is" "green" "+")
triple10
((triple11 triple14) -> (rule2 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
((triple11 ((triple12) -> (rule3 % int2))) -> (rule2 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
((triple11 ((((triple11) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3
Gary is kind.
("Gary" "is" "kind" "+")
triple11
Gary is nice.
("Gary" "is" "nice" "+")
triple12
((triple11) -> (rule6 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
((triple14) -> (rule5 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
triple13
Gary is red.
("Gary" "is" "red" "+")
triple14
((triple12) -> (rule3 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
((((triple11) -> (rule6 % int2))) -> (rule3 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
triple15
Anne is nice.
("Anne" "is" "nice" "+")
((triple1) -> (rule6 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
((triple6) -> (rule3 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
((((triple5) -> (rule6 % int2))) -> (rule3 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
((((triple7) -> (rule1 % int2))) -> (rule3 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
((((triple1) -> (rule6 % int2))) -> (rule3 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
((triple5 ((triple6) -> (rule3 % int2))) -> (rule2 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
((triple5 ((((triple5) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
int3
((triple5 ((((triple7) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
int3
Anne is green.
("Anne" "is" "green" "+")
((triple1 ((((triple1) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
Anne is big.
("Anne" "is" "big" "+")
((((triple1 ((((triple1) -> (rule6 % int4))) -> (rule3 % int3))) -> (rule2 % int2)) triple1) -> (rule4 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3
Anne is nice.
("Anne" "is" "nice" "+")
int4