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