Bob is big. Bob is blue. Bob is quiet. Bob is white. Dave is blue. Dave is quiet. Erin is big. Erin is cold. Erin is nice. Erin is quiet. Erin is white. Erin is young. Big things are cold. Nice, blue things are young. All blue things are nice. All nice things are young. All young things are big. All big, nice things are young. Young, nice things are blue. Nice, cold things are white.
Bob is big.
("Bob" "is" "big" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is white.
("Bob" "is" "white" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is white.
("Erin" "is" "white" "+")
Erin is young.
("Erin" "is" "young" "+")
Big things are cold.
((("something" "is" "big" "+")) -> ("something" "is" "cold" "+"))
Nice, blue things are young.
((("something" "is" "nice" "+") ("something" "is" "blue" "+")) -> ("something" "is" "young" "+"))
All blue things are nice.
((("something" "is" "blue" "+")) -> ("something" "is" "nice" "+"))
All nice things are young.
((("something" "is" "nice" "+")) -> ("something" "is" "young" "+"))
All young things are big.
((("something" "is" "young" "+")) -> ("something" "is" "big" "+"))
All big, nice things are young.
((("something" "is" "big" "+") ("something" "is" "nice" "+")) -> ("something" "is" "young" "+"))
Young, nice things are blue.
((("something" "is" "young" "+") ("something" "is" "nice" "+")) -> ("something" "is" "blue" "+"))
Nice, cold things are white.
((("something" "is" "nice" "+") ("something" "is" "cold" "+")) -> ("something" "is" "white" "+"))
Erin is big.
True
1
proof
[(triple7 OR ((triple12) -> rule5) OR ((((triple9) -> rule4)) -> rule5))]
("Erin" "is" "big" "+")
triple7
((triple12) -> (rule5 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
((((triple9) -> (rule4 % int2))) -> (rule5 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Dave is not quiet.
False
1
inv-proof
[(triple6)]
("Dave" "is" "quiet" "-")
triple6
Erin is blue.
True
3
proof
[(((triple12 triple9) -> rule7) OR ((((triple9) -> rule4) triple9) -> rule7) OR ((((triple7 triple9) -> rule6) triple9) -> rule7))]
("Erin" "is" "blue" "+")
((triple12 triple9) -> (rule7 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
((((triple9) -> (rule4 % int2)) triple9) -> (rule7 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
((((triple7 triple9) -> (rule6 % int2)) triple9) -> (rule7 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Bob is not cold.
False
2
inv-proof
[(((triple1) -> rule1) OR ((((((((triple2) -> rule3)) -> rule4)) -> rule5)) -> rule1) OR ((((((((triple2) -> rule3) triple2) -> rule2)) -> rule5)) -> rule1))]
("Bob" "is" "cold" "-")
((triple1) -> (rule1 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
((((((((triple2) -> (rule3 % int4))) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
Bob is nice.
("Bob" "is" "nice" "+")
int4
((((((((triple2) -> (rule3 % int4)) triple2) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
Bob is nice.
("Bob" "is" "nice" "+")
int4
Bob is young.
True
3
proof
[(((((triple2) -> rule3)) -> rule4) OR ((triple1 ((triple2) -> rule3)) -> rule6) OR ((((triple2) -> rule3) triple2) -> rule2))]
("Bob" "is" "young" "+")
((((triple2) -> (rule3 % int2))) -> (rule4 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
((triple1 ((triple2) -> (rule3 % int2))) -> (rule6 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
((((triple2) -> (rule3 % int2)) triple2) -> (rule2 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Dave is not young.
False
3
inv-proof
[(((((triple5) -> rule3)) -> rule4) OR ((((triple5) -> rule3) triple5) -> rule2))]
("Dave" "is" "young" "-")
((((triple5) -> (rule3 % int2))) -> (rule4 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
((((triple5) -> (rule3 % int2)) triple5) -> (rule2 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is big.
True
4
proof
[(((((((triple5) -> rule3)) -> rule4)) -> rule5) OR ((((((triple5) -> rule3) triple5) -> rule2)) -> rule5))]
("Dave" "is" "big" "+")
((((((triple5) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
((((((triple5) -> (rule3 % int3)) triple5) -> (rule2 % int2))) -> (rule5 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Dave is not big.
False
4
inv-proof
[(((((((triple5) -> rule3)) -> rule4)) -> rule5) OR ((((((triple5) -> rule3) triple5) -> rule2)) -> rule5))]
("Dave" "is" "big" "-")
((((((triple5) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
((((((triple5) -> (rule3 % int3)) triple5) -> (rule2 % int2))) -> (rule5 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
@0: Bob is big.[(triple1 OR ((((((triple2) -> rule3)) -> rule4)) -> rule5) OR ((((((triple2) -> rule3) triple2) -> rule2)) -> rule5))] Bob is blue.[(triple2)] Bob is quiet.[(triple3)] Bob is white.[(triple4 OR ((((triple2) -> rule3) ((triple1) -> rule1)) -> rule8) OR ((((triple2) -> rule3) ((((((((triple2) -> rule3)) -> rule4)) -> rule5)) -> rule1)) -> rule8) OR ((((triple2) -> rule3) ((((((((triple2) -> rule3) triple2) -> rule2)) -> rule5)) -> rule1)) -> rule8))] Dave is blue.[(triple5)] Dave is quiet.[(triple6)] Erin is big.[(triple7 OR ((triple12) -> rule5) OR ((((triple9) -> rule4)) -> rule5))] Erin is cold.[(triple8 OR ((triple7) -> rule1) OR ((((triple12) -> rule5)) -> rule1) OR ((((((triple9) -> rule4)) -> rule5)) -> rule1))] Erin is nice.[(triple9)] Erin is quiet.[(triple10)] Erin is white.[(triple11 OR ((triple9 triple8) -> rule8) OR ((triple9 ((triple7) -> rule1)) -> rule8) OR ((triple9 ((((triple12) -> rule5)) -> rule1)) -> rule8) OR ((triple9 ((((((triple9) -> rule4)) -> rule5)) -> rule1)) -> rule8))] Erin is young.[(triple12 OR ((triple9) -> rule4) OR ((triple7 triple9) -> rule6))] @1: Bob is cold.[(((triple1) -> rule1) OR ((((((((triple2) -> rule3)) -> rule4)) -> rule5)) -> rule1) OR ((((((((triple2) -> rule3) triple2) -> rule2)) -> rule5)) -> rule1))] Bob is nice.[(((triple2) -> rule3))] Dave is nice.[(((triple5) -> rule3))] Erin is blue.[(((triple12 triple9) -> rule7) OR ((((triple9) -> rule4) triple9) -> rule7) OR ((((triple7 triple9) -> rule6) triple9) -> rule7))] @2: Bob is young.[(((((triple2) -> rule3)) -> rule4) OR ((triple1 ((triple2) -> rule3)) -> rule6) OR ((((triple2) -> rule3) triple2) -> rule2))] Dave is young.[(((((triple5) -> rule3)) -> rule4) OR ((((triple5) -> rule3) triple5) -> rule2))] @3: Dave is big.[(((((((triple5) -> rule3)) -> rule4)) -> rule5) OR ((((((triple5) -> rule3) triple5) -> rule2)) -> rule5))] @4: Dave is cold.[(((((((((triple5) -> rule3)) -> rule4)) -> rule5)) -> rule1) OR ((((((((triple5) -> rule3) triple5) -> rule2)) -> rule5)) -> rule1))] @5: Dave is white.[(((((triple5) -> rule3) ((((((((triple5) -> rule3)) -> rule4)) -> rule5)) -> rule1)) -> rule8) OR ((((triple5) -> rule3) ((((((((triple5) -> rule3) triple5) -> rule2)) -> rule5)) -> rule1)) -> rule8))]
Bob is big.
("Bob" "is" "big" "+")
triple1
((((((triple2) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
int3
((((((triple2) -> (rule3 % int3)) triple2) -> (rule2 % int2))) -> (rule5 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
int3
Bob is blue.
("Bob" "is" "blue" "+")
triple2
Bob is quiet.
("Bob" "is" "quiet" "+")
triple3
Bob is white.
("Bob" "is" "white" "+")
triple4
((((triple2) -> (rule3 % int3)) ((triple1) -> (rule1 % int2))) -> (rule8 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
int3
((((triple2) -> (rule3 % int5)) ((((((((triple2) -> (rule3 % int5))) -> (rule4 % int4))) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
Bob is young.
("Bob" "is" "young" "+")
int4
Bob is nice.
("Bob" "is" "nice" "+")
int5
((((triple2) -> (rule3 % int5)) ((((((((triple2) -> (rule3 % int5)) triple2) -> (rule2 % int4))) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
Bob is young.
("Bob" "is" "young" "+")
int4
Bob is nice.
("Bob" "is" "nice" "+")
int5
Dave is blue.
("Dave" "is" "blue" "+")
triple5
Dave is quiet.
("Dave" "is" "quiet" "+")
triple6
Erin is big.
("Erin" "is" "big" "+")
triple7
((triple12) -> (rule5 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
((((triple9) -> (rule4 % int2))) -> (rule5 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
triple8
((triple7) -> (rule1 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
((((triple12) -> (rule5 % int2))) -> (rule1 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
((((((triple9) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
Erin is nice.
("Erin" "is" "nice" "+")
triple9
Erin is quiet.
("Erin" "is" "quiet" "+")
triple10
Erin is white.
("Erin" "is" "white" "+")
triple11
((triple9 triple8) -> (rule8 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
((triple9 ((triple7) -> (rule1 % int2))) -> (rule8 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
((triple9 ((((triple12) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3
((triple9 ((((((triple9) -> (rule4 % int4))) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3
Erin is young.
("Erin" "is" "young" "+")
int4
Erin is young.
("Erin" "is" "young" "+")
triple12
((triple9) -> (rule4 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
((triple7 triple9) -> (rule6 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
((triple1) -> (rule1 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
((((((((triple2) -> (rule3 % int4))) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
Bob is nice.
("Bob" "is" "nice" "+")
int4
((((((((triple2) -> (rule3 % int4)) triple2) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
Bob is nice.
("Bob" "is" "nice" "+")
int4
Bob is nice.
("Bob" "is" "nice" "+")
((triple2) -> (rule3 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
((triple5) -> (rule3 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
((triple12 triple9) -> (rule7 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
((((triple9) -> (rule4 % int2)) triple9) -> (rule7 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
((((triple7 triple9) -> (rule6 % int2)) triple9) -> (rule7 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
((((triple2) -> (rule3 % int2))) -> (rule4 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
((triple1 ((triple2) -> (rule3 % int2))) -> (rule6 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
((((triple2) -> (rule3 % int2)) triple2) -> (rule2 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
((((triple5) -> (rule3 % int2))) -> (rule4 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
((((triple5) -> (rule3 % int2)) triple5) -> (rule2 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
((((((triple5) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
((((((triple5) -> (rule3 % int3)) triple5) -> (rule2 % int2))) -> (rule5 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Dave is cold.
("Dave" "is" "cold" "+")
((((((((triple5) -> (rule3 % int4))) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Dave is nice.
("Dave" "is" "nice" "+")
int4
((((((((triple5) -> (rule3 % int4)) triple5) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Dave is nice.
("Dave" "is" "nice" "+")
int4
Dave is white.
("Dave" "is" "white" "+")
((((triple5) -> (rule3 % int5)) ((((((((triple5) -> (rule3 % int5))) -> (rule4 % int4))) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Dave is young.
("Dave" "is" "young" "+")
int4
Dave is nice.
("Dave" "is" "nice" "+")
int5
((((triple5) -> (rule3 % int5)) ((((((((triple5) -> (rule3 % int5)) triple5) -> (rule2 % int4))) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Dave is young.
("Dave" "is" "young" "+")
int4
Dave is nice.
("Dave" "is" "nice" "+")
int5