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