Erin is nice. Erin is quiet. Erin is smart. Fiona is big. Fiona is nice. Fiona is quiet. Fiona is red. Fiona is round. Fiona is smart. Fiona is white. If Erin is quiet and Erin is red then Erin is nice. Nice things are red. All round, big things are smart. All big, quiet things are white. White, nice things are red. If Erin is red and Erin is quiet then Erin is big. If Erin is nice then Erin is red. If Fiona is smart and Fiona is nice then Fiona is red.
Erin is nice.
("Erin" "is" "nice" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Fiona is round.
("Fiona" "is" "round" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Fiona is white.
("Fiona" "is" "white" "+")
If Erin is quiet and Erin is red then Erin is nice.
((("Erin" "is" "quiet" "+") ("Erin" "is" "red" "+")) -> ("Erin" "is" "nice" "+"))
Nice things are red.
((("something" "is" "nice" "+")) -> ("something" "is" "red" "+"))
All round, big things are smart.
((("something" "is" "round" "+") ("something" "is" "big" "+")) -> ("something" "is" "smart" "+"))
All big, quiet things are white.
((("something" "is" "big" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "white" "+"))
White, nice things are red.
((("something" "is" "white" "+") ("something" "is" "nice" "+")) -> ("something" "is" "red" "+"))
If Erin is red and Erin is quiet then Erin is big.
((("Erin" "is" "red" "+") ("Erin" "is" "quiet" "+")) -> ("Erin" "is" "big" "+"))
If Erin is nice then Erin is red.
((("Erin" "is" "nice" "+")) -> ("Erin" "is" "red" "+"))
If Fiona is smart and Fiona is nice then Fiona is red.
((("Fiona" "is" "smart" "+") ("Fiona" "is" "nice" "+")) -> ("Fiona" "is" "red" "+"))
Fiona is red.
True
1
proof
[(triple7 OR ((triple5) -> rule2) OR ((triple10 triple5) -> rule5) OR ((triple9 triple5) -> rule8) OR ((((triple4 triple6) -> rule4) triple5) -> rule5) OR ((((triple8 triple4) -> rule3) triple5) -> rule8))]
("Fiona" "is" "red" "+")
triple7
((triple5) -> (rule2 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
((triple10 triple5) -> (rule5 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
((triple9 triple5) -> (rule8 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
((((triple4 triple6) -> (rule4 % int2)) triple5) -> (rule5 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
((((triple8 triple4) -> (rule3 % int2)) triple5) -> (rule8 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is not white.
False
1
inv-proof
[(triple10 OR ((triple4 triple6) -> rule4))]
("Fiona" "is" "white" "-")
triple10
((triple4 triple6) -> (rule4 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Erin is red.
True
2
proof
[(((triple1) -> rule2) OR ((triple1) -> rule7))]
("Erin" "is" "red" "+")
((triple1) -> (rule2 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
((triple1) -> (rule7 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is not red.
False
2
inv-proof
[(((triple1) -> rule2) OR ((triple1) -> rule7))]
("Erin" "is" "red" "-")
((triple1) -> (rule2 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
((triple1) -> (rule7 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is big.
True
4
proof
[(((((triple1) -> rule2) triple2) -> rule6) OR ((((triple1) -> rule7) triple2) -> rule6))]
("Erin" "is" "big" "+")
((((triple1) -> (rule2 % int2)) triple2) -> (rule6 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
((((triple1) -> (rule7 % int2)) triple2) -> (rule6 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is not big.
False
4
inv-proof
[(((((triple1) -> rule2) triple2) -> rule6) OR ((((triple1) -> rule7) triple2) -> rule6))]
("Erin" "is" "big" "-")
((((triple1) -> (rule2 % int2)) triple2) -> (rule6 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
((((triple1) -> (rule7 % int2)) triple2) -> (rule6 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is white.
True
6
proof
[(((((((triple1) -> rule2) triple2) -> rule6) triple2) -> rule4) OR ((((((triple1) -> rule7) triple2) -> rule6) triple2) -> rule4))]
("Erin" "is" "white" "+")
((((((triple1) -> (rule2 % int3)) triple2) -> (rule6 % int2)) triple2) -> (rule4 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
((((((triple1) -> (rule7 % int3)) triple2) -> (rule6 % int2)) triple2) -> (rule4 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
Erin is not white.
False
6
inv-proof
[(((((((triple1) -> rule2) triple2) -> rule6) triple2) -> rule4) OR ((((((triple1) -> rule7) triple2) -> rule6) triple2) -> rule4))]
("Erin" "is" "white" "-")
((((((triple1) -> (rule2 % int3)) triple2) -> (rule6 % int2)) triple2) -> (rule4 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
((((((triple1) -> (rule7 % int3)) triple2) -> (rule6 % int2)) triple2) -> (rule4 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
@0: Erin is nice.[(triple1)] Erin is quiet.[(triple2)] Erin is smart.[(triple3)] Fiona is big.[(triple4)] Fiona is nice.[(triple5)] Fiona is quiet.[(triple6)] Fiona is red.[(triple7 OR ((triple5) -> rule2) OR ((triple10 triple5) -> rule5) OR ((triple9 triple5) -> rule8) OR ((((triple4 triple6) -> rule4) triple5) -> rule5) OR ((((triple8 triple4) -> rule3) triple5) -> rule8))] Fiona is round.[(triple8)] Fiona is smart.[(triple9 OR ((triple8 triple4) -> rule3))] Fiona is white.[(triple10 OR ((triple4 triple6) -> rule4))] @1: Erin is red.[(((triple1) -> rule2) OR ((triple1) -> rule7))] @2: Erin is big.[(((((triple1) -> rule2) triple2) -> rule6) OR ((((triple1) -> rule7) triple2) -> rule6))] @3: Erin is white.[(((((((triple1) -> rule2) triple2) -> rule6) triple2) -> rule4) OR ((((((triple1) -> rule7) triple2) -> rule6) triple2) -> rule4))]
Erin is nice.
("Erin" "is" "nice" "+")
triple1
Erin is quiet.
("Erin" "is" "quiet" "+")
triple2
Erin is smart.
("Erin" "is" "smart" "+")
triple3
Fiona is big.
("Fiona" "is" "big" "+")
triple4
Fiona is nice.
("Fiona" "is" "nice" "+")
triple5
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple6
Fiona is red.
("Fiona" "is" "red" "+")
triple7
((triple5) -> (rule2 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
((triple10 triple5) -> (rule5 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
((triple9 triple5) -> (rule8 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
((((triple4 triple6) -> (rule4 % int2)) triple5) -> (rule5 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
((((triple8 triple4) -> (rule3 % int2)) triple5) -> (rule8 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is round.
("Fiona" "is" "round" "+")
triple8
Fiona is smart.
("Fiona" "is" "smart" "+")
triple9
((triple8 triple4) -> (rule3 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
triple10
((triple4 triple6) -> (rule4 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
((triple1) -> (rule2 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
((triple1) -> (rule7 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
((((triple1) -> (rule2 % int2)) triple2) -> (rule6 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
((((triple1) -> (rule7 % int2)) triple2) -> (rule6 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
((((((triple1) -> (rule2 % int3)) triple2) -> (rule6 % int2)) triple2) -> (rule4 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
((((((triple1) -> (rule7 % int3)) triple2) -> (rule6 % int2)) triple2) -> (rule4 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3