Charlie is big. Charlie is kind. Charlie is nice. Charlie is red. Charlie is white. Dave is big. Dave is blue. Dave is kind. Dave is red. Dave is white. Erin is blue. Erin is red. Kind, red people are white. Smart people are kind. Kind people are big. All big, smart people are white. Red people are smart. All big people are nice.
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is white.
("Dave" "is" "white" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is red.
("Erin" "is" "red" "+")
Kind, red people are white.
((("someone" "is" "kind" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "white" "+"))
Smart people are kind.
((("someone" "is" "smart" "+")) -> ("someone" "is" "kind" "+"))
Kind people are big.
((("someone" "is" "kind" "+")) -> ("someone" "is" "big" "+"))
All big, smart people are white.
((("someone" "is" "big" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "white" "+"))
Red people are smart.
((("someone" "is" "red" "+")) -> ("someone" "is" "smart" "+"))
All big people are nice.
((("someone" "is" "big" "+")) -> ("someone" "is" "nice" "+"))
Dave is white.
True
1
proof
[(triple10 OR ((triple8 triple9) -> rule1) OR ((triple6 ((triple9) -> rule5)) -> rule4) OR ((((triple8) -> rule3) ((triple9) -> rule5)) -> rule4) OR ((((((triple9) -> rule5)) -> rule2) triple9) -> rule1) OR ((((((((triple9) -> rule5)) -> rule2)) -> rule3) ((triple9) -> rule5)) -> rule4))]
("Dave" "is" "white" "+")
triple10
((triple8 triple9) -> (rule1 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
((triple6 ((triple9) -> (rule5 % int2))) -> (rule4 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
((((triple8) -> (rule3 % int3)) ((triple9) -> (rule5 % int2))) -> (rule4 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
((((((triple9) -> (rule5 % int3))) -> (rule2 % int2)) triple9) -> (rule1 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
((((((((triple9) -> (rule5 % int4))) -> (rule2 % int3))) -> (rule3 % int2)) ((triple9) -> (rule5 % int4))) -> (rule4 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
Dave is smart.
("Dave" "is" "smart" "+")
int4
Charlie is not red.
False
1
inv-proof
[(triple4)]
("Charlie" "is" "red" "-")
triple4
Erin is smart.
True
2
proof
[(((triple12) -> rule5))]
("Erin" "is" "smart" "+")
((triple12) -> (rule5 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Dave is not nice.
False
2
inv-proof
[(((triple6) -> rule6) OR ((((triple8) -> rule3)) -> rule6) OR ((((((((triple9) -> rule5)) -> rule2)) -> rule3)) -> rule6))]
("Dave" "is" "nice" "-")
((triple6) -> (rule6 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
((((triple8) -> (rule3 % int2))) -> (rule6 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
((((((((triple9) -> (rule5 % int4))) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
Dave is smart.
("Dave" "is" "smart" "+")
int4
Erin is kind.
True
3
proof
[(((((triple12) -> rule5)) -> rule2))]
("Erin" "is" "kind" "+")
((((triple12) -> (rule5 % int2))) -> (rule2 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is not kind.
False
3
inv-proof
[(((((triple12) -> rule5)) -> rule2))]
("Erin" "is" "kind" "-")
((((triple12) -> (rule5 % int2))) -> (rule2 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is big.
True
4
proof
[(((((((triple12) -> rule5)) -> rule2)) -> rule3))]
("Erin" "is" "big" "+")
((((((triple12) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Erin is not big.
False
4
inv-proof
[(((((((triple12) -> rule5)) -> rule2)) -> rule3))]
("Erin" "is" "big" "-")
((((((triple12) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
@0: Charlie is big.[(triple1 OR ((triple2) -> rule3) OR ((((((triple4) -> rule5)) -> rule2)) -> rule3))] Charlie is kind.[(triple2 OR ((((triple4) -> rule5)) -> rule2))] Charlie is nice.[(triple3 OR ((triple1) -> rule6) OR ((((triple2) -> rule3)) -> rule6) OR ((((((((triple4) -> rule5)) -> rule2)) -> rule3)) -> rule6))] Charlie is red.[(triple4)] Charlie is white.[(triple5 OR ((triple2 triple4) -> rule1) OR ((triple1 ((triple4) -> rule5)) -> rule4) OR ((((triple2) -> rule3) ((triple4) -> rule5)) -> rule4) OR ((((((triple4) -> rule5)) -> rule2) triple4) -> rule1) OR ((((((((triple4) -> rule5)) -> rule2)) -> rule3) ((triple4) -> rule5)) -> rule4))] Dave is big.[(triple6 OR ((triple8) -> rule3) OR ((((((triple9) -> rule5)) -> rule2)) -> rule3))] Dave is blue.[(triple7)] Dave is kind.[(triple8 OR ((((triple9) -> rule5)) -> rule2))] Dave is red.[(triple9)] Dave is white.[(triple10 OR ((triple8 triple9) -> rule1) OR ((triple6 ((triple9) -> rule5)) -> rule4) OR ((((triple8) -> rule3) ((triple9) -> rule5)) -> rule4) OR ((((((triple9) -> rule5)) -> rule2) triple9) -> rule1) OR ((((((((triple9) -> rule5)) -> rule2)) -> rule3) ((triple9) -> rule5)) -> rule4))] Erin is blue.[(triple11)] Erin is red.[(triple12)] @1: Charlie is smart.[(((triple4) -> rule5))] Dave is nice.[(((triple6) -> rule6) OR ((((triple8) -> rule3)) -> rule6) OR ((((((((triple9) -> rule5)) -> rule2)) -> rule3)) -> rule6))] Dave is smart.[(((triple9) -> rule5))] Erin is smart.[(((triple12) -> rule5))] @2: Erin is kind.[(((((triple12) -> rule5)) -> rule2))] @3: Erin is big.[(((((((triple12) -> rule5)) -> rule2)) -> rule3))] Erin is white.[(((((((triple12) -> rule5)) -> rule2) triple12) -> rule1) OR ((((((((triple12) -> rule5)) -> rule2)) -> rule3) ((triple12) -> rule5)) -> rule4))] @4: Erin is nice.[(((((((((triple12) -> rule5)) -> rule2)) -> rule3)) -> rule6))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
((triple2) -> (rule3 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
((((((triple4) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
Charlie is kind.
("Charlie" "is" "kind" "+")
triple2
((((triple4) -> (rule5 % int2))) -> (rule2 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
triple3
((triple1) -> (rule6 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
((((triple2) -> (rule3 % int2))) -> (rule6 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
((((((((triple4) -> (rule5 % int4))) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
Charlie is smart.
("Charlie" "is" "smart" "+")
int4
Charlie is red.
("Charlie" "is" "red" "+")
triple4
Charlie is white.
("Charlie" "is" "white" "+")
triple5
((triple2 triple4) -> (rule1 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
((triple1 ((triple4) -> (rule5 % int2))) -> (rule4 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
((((triple2) -> (rule3 % int3)) ((triple4) -> (rule5 % int2))) -> (rule4 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
((((((triple4) -> (rule5 % int3))) -> (rule2 % int2)) triple4) -> (rule1 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
((((((((triple4) -> (rule5 % int4))) -> (rule2 % int3))) -> (rule3 % int2)) ((triple4) -> (rule5 % int4))) -> (rule4 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
Charlie is smart.
("Charlie" "is" "smart" "+")
int4
Dave is big.
("Dave" "is" "big" "+")
triple6
((triple8) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
((((((triple9) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
Dave is blue.
("Dave" "is" "blue" "+")
triple7
Dave is kind.
("Dave" "is" "kind" "+")
triple8
((((triple9) -> (rule5 % int2))) -> (rule2 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
triple9
Dave is white.
("Dave" "is" "white" "+")
triple10
((triple8 triple9) -> (rule1 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
((triple6 ((triple9) -> (rule5 % int2))) -> (rule4 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
((((triple8) -> (rule3 % int3)) ((triple9) -> (rule5 % int2))) -> (rule4 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
((((((triple9) -> (rule5 % int3))) -> (rule2 % int2)) triple9) -> (rule1 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
((((((((triple9) -> (rule5 % int4))) -> (rule2 % int3))) -> (rule3 % int2)) ((triple9) -> (rule5 % int4))) -> (rule4 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
Dave is smart.
("Dave" "is" "smart" "+")
int4
Erin is blue.
("Erin" "is" "blue" "+")
triple11
Erin is red.
("Erin" "is" "red" "+")
triple12
Charlie is smart.
("Charlie" "is" "smart" "+")
((triple4) -> (rule5 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
((triple6) -> (rule6 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
((((triple8) -> (rule3 % int2))) -> (rule6 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
((((((((triple9) -> (rule5 % int4))) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
Dave is smart.
("Dave" "is" "smart" "+")
int4
Dave is smart.
("Dave" "is" "smart" "+")
((triple9) -> (rule5 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
((triple12) -> (rule5 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
((((triple12) -> (rule5 % int2))) -> (rule2 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
((((((triple12) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Erin is white.
("Erin" "is" "white" "+")
((((((triple12) -> (rule5 % int3))) -> (rule2 % int2)) triple12) -> (rule1 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
((((((((triple12) -> (rule5 % int4))) -> (rule2 % int3))) -> (rule3 % int2)) ((triple12) -> (rule5 % int4))) -> (rule4 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Erin is smart.
("Erin" "is" "smart" "+")
int4
Erin is nice.
("Erin" "is" "nice" "+")
((((((((triple12) -> (rule5 % int4))) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Erin is smart.
("Erin" "is" "smart" "+")
int4