Charlie is big. Charlie is cold. Charlie is green. Charlie is nice. Charlie is red. Charlie is round. Charlie is white. All cold people are big. All white people are cold.
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is white.
("Charlie" "is" "white" "+")
All cold people are big.
((("someone" "is" "cold" "+")) -> ("someone" "is" "big" "+"))
All white people are cold.
((("someone" "is" "white" "+")) -> ("someone" "is" "cold" "+"))
Charlie is cold.
True
1
proof
[(triple2 OR ((triple7) -> rule2))]
("Charlie" "is" "cold" "+")
triple2
((triple7) -> (rule2 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is not round.
False
1
inv-proof
[(triple6)]
("Charlie" "is" "round" "-")
triple6
@0: Charlie is big.[(triple1 OR ((triple2) -> rule1) OR ((((triple7) -> rule2)) -> rule1))] Charlie is cold.[(triple2 OR ((triple7) -> rule2))] Charlie is green.[(triple3)] Charlie is nice.[(triple4)] Charlie is red.[(triple5)] Charlie is round.[(triple6)] Charlie is white.[(triple7)]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
((triple2) -> (rule1 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
((((triple7) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
triple2
((triple7) -> (rule2 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
triple3
Charlie is nice.
("Charlie" "is" "nice" "+")
triple4
Charlie is red.
("Charlie" "is" "red" "+")
triple5
Charlie is round.
("Charlie" "is" "round" "+")
triple6
Charlie is white.
("Charlie" "is" "white" "+")
triple7