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