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