Erin is blue. Erin is cold. Erin is kind. Erin is nice. Erin is red. Erin is round. Erin is smart. Harry is cold. Harry is kind. Harry is nice. Harry is red. Harry is smart. If Harry is cold then Harry is kind. Red, nice people are cold. Blue people are red. Red people are blue. All smart people are blue. Blue, nice people are round.
Erin is blue.
("Erin" "is" "blue" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is round.
("Erin" "is" "round" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is smart.
("Harry" "is" "smart" "+")
If Harry is cold then Harry is kind.
((("Harry" "is" "cold" "+")) -> ("Harry" "is" "kind" "+"))
Red, nice people are cold.
((("someone" "is" "red" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "cold" "+"))
Blue people are red.
((("someone" "is" "blue" "+")) -> ("someone" "is" "red" "+"))
Red people are blue.
((("someone" "is" "red" "+")) -> ("someone" "is" "blue" "+"))
All smart people are blue.
((("someone" "is" "smart" "+")) -> ("someone" "is" "blue" "+"))
Blue, nice people are round.
((("someone" "is" "blue" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "round" "+"))
Erin is kind.
True
1
proof
[(triple3)]
("Erin" "is" "kind" "+")
triple3
Erin is not red.
False
1
inv-proof
[(triple5 OR ((triple1) -> rule3) OR ((((triple7) -> rule5)) -> rule3))]
("Erin" "is" "red" "-")
triple5
((triple1) -> (rule3 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
((((triple7) -> (rule5 % int2))) -> (rule3 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Harry is blue.
True
2
proof
[(((triple11) -> rule4) OR ((triple12) -> rule5))]
("Harry" "is" "blue" "+")
((triple11) -> (rule4 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
((triple12) -> (rule5 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is not blue.
False
2
inv-proof
[(((triple11) -> rule4) OR ((triple12) -> rule5))]
("Harry" "is" "blue" "-")
((triple11) -> (rule4 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
((triple12) -> (rule5 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is round.
True
4
proof
[(((((triple11) -> rule4) triple10) -> rule6) OR ((((triple12) -> rule5) triple10) -> rule6))]
("Harry" "is" "round" "+")
((((triple11) -> (rule4 % int2)) triple10) -> (rule6 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
((((triple12) -> (rule5 % int2)) triple10) -> (rule6 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is not round.
False
4
inv-proof
[(((((triple11) -> rule4) triple10) -> rule6) OR ((((triple12) -> rule5) triple10) -> rule6))]
("Harry" "is" "round" "-")
((((triple11) -> (rule4 % int2)) triple10) -> (rule6 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
((((triple12) -> (rule5 % int2)) triple10) -> (rule6 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
@0: Erin is blue.[(triple1 OR ((triple5) -> rule4) OR ((triple7) -> rule5))] Erin is cold.[(triple2 OR ((triple5 triple4) -> rule2) OR ((((triple1) -> rule3) triple4) -> rule2) OR ((((((triple7) -> rule5)) -> rule3) triple4) -> rule2))] Erin is kind.[(triple3)] Erin is nice.[(triple4)] Erin is red.[(triple5 OR ((triple1) -> rule3) OR ((((triple7) -> rule5)) -> rule3))] Erin is round.[(triple6 OR ((triple1 triple4) -> rule6) OR ((((triple5) -> rule4) triple4) -> rule6) OR ((((triple7) -> rule5) triple4) -> rule6))] Erin is smart.[(triple7)] Harry is cold.[(triple8 OR ((triple11 triple10) -> rule2) OR ((((((triple12) -> rule5)) -> rule3) triple10) -> rule2))] Harry is kind.[(triple9 OR ((triple8) -> rule1) OR ((((triple11 triple10) -> rule2)) -> rule1) OR ((((((((triple12) -> rule5)) -> rule3) triple10) -> rule2)) -> rule1))] Harry is nice.[(triple10)] Harry is red.[(triple11 OR ((((triple12) -> rule5)) -> rule3))] Harry is smart.[(triple12)] @1: Harry is blue.[(((triple11) -> rule4) OR ((triple12) -> rule5))] @2: Harry is round.[(((((triple11) -> rule4) triple10) -> rule6) OR ((((triple12) -> rule5) triple10) -> rule6))]
Erin is blue.
("Erin" "is" "blue" "+")
triple1
((triple5) -> (rule4 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
((triple7) -> (rule5 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
triple2
((triple5 triple4) -> (rule2 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
((((triple1) -> (rule3 % int2)) triple4) -> (rule2 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
((((((triple7) -> (rule5 % int3))) -> (rule3 % int2)) triple4) -> (rule2 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3
Erin is kind.
("Erin" "is" "kind" "+")
triple3
Erin is nice.
("Erin" "is" "nice" "+")
triple4
Erin is red.
("Erin" "is" "red" "+")
triple5
((triple1) -> (rule3 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
((((triple7) -> (rule5 % int2))) -> (rule3 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
triple6
((triple1 triple4) -> (rule6 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
((((triple5) -> (rule4 % int2)) triple4) -> (rule6 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
((((triple7) -> (rule5 % int2)) triple4) -> (rule6 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
triple7
Harry is cold.
("Harry" "is" "cold" "+")
triple8
((triple11 triple10) -> (rule2 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
((((((triple12) -> (rule5 % int3))) -> (rule3 % int2)) triple10) -> (rule2 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
Harry is kind.
("Harry" "is" "kind" "+")
triple9
((triple8) -> (rule1 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
((((triple11 triple10) -> (rule2 % int2))) -> (rule1 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
((((((((triple12) -> (rule5 % int4))) -> (rule3 % int3)) triple10) -> (rule2 % int2))) -> (rule1 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
int3
Harry is blue.
("Harry" "is" "blue" "+")
int4
Harry is nice.
("Harry" "is" "nice" "+")
triple10
Harry is red.
("Harry" "is" "red" "+")
triple11
((((triple12) -> (rule5 % int2))) -> (rule3 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
triple12
Harry is blue.
("Harry" "is" "blue" "+")
((triple11) -> (rule4 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
((triple12) -> (rule5 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
((((triple11) -> (rule4 % int2)) triple10) -> (rule6 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
((((triple12) -> (rule5 % int2)) triple10) -> (rule6 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2