Bob is big. Bob is blue. Bob is cold. Bob is not kind. Bob is nice. Bob is not red. Bob is white. Charlie is big. Charlie is blue. Charlie is cold. Charlie is not kind. Charlie is nice. Charlie is red. Charlie is white. If someone is cold then they are big.
Bob is big.
("Bob" "is" "big" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is not kind.
("Bob" "is" "kind" "-")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is not red.
("Bob" "is" "red" "-")
Bob is white.
("Bob" "is" "white" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is not kind.
("Charlie" "is" "kind" "-")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is white.
("Charlie" "is" "white" "+")
If someone is cold then they are big.
((("someone" "is" "cold" "+")) -> ("someone" "is" "big" "+"))
Charlie is blue.
True
1
proof
[(triple9)]
("Charlie" "is" "blue" "+")
triple9
Bob is not white.
False
1
inv-proof
[(triple7)]
("Bob" "is" "white" "-")
triple7
@0: Bob is big.[(triple1 OR ((triple3) -> rule1))] Bob is blue.[(triple2)] Bob is cold.[(triple3)] Bob is nice.[(triple5)] Bob is not kind.[(triple4)] Bob is not red.[(triple6)] Bob is white.[(triple7)] Charlie is big.[(triple8 OR ((triple10) -> rule1))] Charlie is blue.[(triple9)] Charlie is cold.[(triple10)] Charlie is nice.[(triple12)] Charlie is not kind.[(triple11)] Charlie is red.[(triple13)] Charlie is white.[(triple14)]
Bob is big.
("Bob" "is" "big" "+")
triple1
((triple3) -> (rule1 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
triple2
Bob is cold.
("Bob" "is" "cold" "+")
triple3
Bob is nice.
("Bob" "is" "nice" "+")
triple5
Bob is not kind.
("Bob" "is" "kind" "-")
triple4
Bob is not red.
("Bob" "is" "red" "-")
triple6
Bob is white.
("Bob" "is" "white" "+")
triple7
Charlie is big.
("Charlie" "is" "big" "+")
triple8
((triple10) -> (rule1 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
triple9
Charlie is cold.
("Charlie" "is" "cold" "+")
triple10
Charlie is nice.
("Charlie" "is" "nice" "+")
triple12
Charlie is not kind.
("Charlie" "is" "kind" "-")
triple11
Charlie is red.
("Charlie" "is" "red" "+")
triple13
Charlie is white.
("Charlie" "is" "white" "+")
triple14