Charlie is cold. Charlie is red. Charlie is rough. If Charlie is not red then Charlie is round. Cold people are big. If someone is rough and cold then they are blue. Big people are rough. All nice, rough people are round. All rough, nice people are round. If someone is blue and not big then they are not nice. Big people are nice.
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
If Charlie is not red then Charlie is round.
((("Charlie" "is" "red" "~")) -> ("Charlie" "is" "round" "+"))
Cold people are big.
((("someone" "is" "cold" "+")) -> ("someone" "is" "big" "+"))
If someone is rough and cold then they are blue.
((("someone" "is" "rough" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "blue" "+"))
Big people are rough.
((("someone" "is" "big" "+")) -> ("someone" "is" "rough" "+"))
All nice, rough people are round.
((("someone" "is" "nice" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "round" "+"))
All rough, nice people are round.
((("someone" "is" "rough" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "round" "+"))
If someone is blue and not big then they are not nice.
((("someone" "is" "blue" "+") ("someone" "is" "big" "~")) -> ("someone" "is" "nice" "-"))
Big people are nice.
((("someone" "is" "big" "+")) -> ("someone" "is" "nice" "+"))
Charlie is rough.
True
1
proof
[(triple3 OR ((((triple1) -> rule2)) -> rule4))]
("Charlie" "is" "rough" "+")
triple3
((((triple1) -> (rule2 % int2))) -> (rule4 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is not red.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "red" "-")
triple2
Charlie is blue.
True
3
proof
[(((triple3 triple1) -> rule3) OR ((((((triple1) -> rule2)) -> rule4) triple1) -> rule3))]
("Charlie" "is" "blue" "+")
((triple3 triple1) -> (rule3 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
((((((triple1) -> (rule2 % int3))) -> (rule4 % int2)) triple1) -> (rule3 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
Charlie is not big.
False
2
inv-proof
[(((triple1) -> rule2))]
("Charlie" "is" "big" "-")
((triple1) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is nice.
True
3
proof
[(((((triple1) -> rule2)) -> rule8))]
("Charlie" "is" "nice" "+")
((((triple1) -> (rule2 % int2))) -> (rule8 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is not nice.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule8))]
("Charlie" "is" "nice" "-")
((((triple1) -> (rule2 % int2))) -> (rule8 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is round.
True
5
proof
[(((triple3 ((((triple1) -> rule2)) -> rule8)) -> rule6) OR ((((((triple1) -> rule2)) -> rule8) triple3) -> rule5) OR ((((((triple1) -> rule2)) -> rule4) ((((triple1) -> rule2)) -> rule8)) -> rule6) OR ((((((triple1) -> rule2)) -> rule8) ((((triple1) -> rule2)) -> rule4)) -> rule5))]
("Charlie" "is" "round" "+")
((triple3 ((((triple1) -> (rule2 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
((((((triple1) -> (rule2 % int3))) -> (rule8 % int2)) triple3) -> (rule5 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
((((((triple1) -> (rule2 % int4))) -> (rule4 % int3)) ((((triple1) -> (rule2 % int4))) -> (rule8 % int2))) -> (rule6 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Charlie is big.
("Charlie" "is" "big" "+")
int4
((((((triple1) -> (rule2 % int4))) -> (rule8 % int3)) ((((triple1) -> (rule2 % int4))) -> (rule4 % int2))) -> (rule5 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
Charlie is big.
("Charlie" "is" "big" "+")
int4
Charlie is not round.
False
5
inv-proof
[(((triple3 ((((triple1) -> rule2)) -> rule8)) -> rule6) OR ((((((triple1) -> rule2)) -> rule8) triple3) -> rule5) OR ((((((triple1) -> rule2)) -> rule4) ((((triple1) -> rule2)) -> rule8)) -> rule6) OR ((((((triple1) -> rule2)) -> rule8) ((((triple1) -> rule2)) -> rule4)) -> rule5))]
("Charlie" "is" "round" "-")
((triple3 ((((triple1) -> (rule2 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
((((((triple1) -> (rule2 % int3))) -> (rule8 % int2)) triple3) -> (rule5 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
((((((triple1) -> (rule2 % int4))) -> (rule4 % int3)) ((((triple1) -> (rule2 % int4))) -> (rule8 % int2))) -> (rule6 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Charlie is big.
("Charlie" "is" "big" "+")
int4
((((((triple1) -> (rule2 % int4))) -> (rule8 % int3)) ((((triple1) -> (rule2 % int4))) -> (rule4 % int2))) -> (rule5 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
Charlie is big.
("Charlie" "is" "big" "+")
int4
@0: Charlie is cold.[(triple1)] Charlie is red.[(triple2)] Charlie is rough.[(triple3 OR ((((triple1) -> rule2)) -> rule4))] @1: Charlie is big.[(((triple1) -> rule2))] Charlie is blue.[(((triple3 triple1) -> rule3) OR ((((((triple1) -> rule2)) -> rule4) triple1) -> rule3))] @2: Charlie is nice.[(((((triple1) -> rule2)) -> rule8))] @3: Charlie is round.[(((triple3 ((((triple1) -> rule2)) -> rule8)) -> rule6) OR ((((((triple1) -> rule2)) -> rule8) triple3) -> rule5) OR ((((((triple1) -> rule2)) -> rule4) ((((triple1) -> rule2)) -> rule8)) -> rule6) OR ((((((triple1) -> rule2)) -> rule8) ((((triple1) -> rule2)) -> rule4)) -> rule5))]
Charlie is cold.
("Charlie" "is" "cold" "+")
triple1
Charlie is red.
("Charlie" "is" "red" "+")
triple2
Charlie is rough.
("Charlie" "is" "rough" "+")
triple3
((((triple1) -> (rule2 % int2))) -> (rule4 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
((triple1) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
((triple3 triple1) -> (rule3 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
((((((triple1) -> (rule2 % int3))) -> (rule4 % int2)) triple1) -> (rule3 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
Charlie is nice.
("Charlie" "is" "nice" "+")
((((triple1) -> (rule2 % int2))) -> (rule8 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
((triple3 ((((triple1) -> (rule2 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
((((((triple1) -> (rule2 % int3))) -> (rule8 % int2)) triple3) -> (rule5 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
((((((triple1) -> (rule2 % int4))) -> (rule4 % int3)) ((((triple1) -> (rule2 % int4))) -> (rule8 % int2))) -> (rule6 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Charlie is big.
("Charlie" "is" "big" "+")
int4
((((((triple1) -> (rule2 % int4))) -> (rule8 % int3)) ((((triple1) -> (rule2 % int4))) -> (rule4 % int2))) -> (rule5 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
Charlie is big.
("Charlie" "is" "big" "+")
int4