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