Charlie is big. Charlie is blue. Charlie is cold. Charlie is green. Charlie is kind. Charlie is quiet. Charlie is red. Harry is big. Harry is blue. Harry is cold. Harry is green. Harry is kind. Harry is quiet. Harry is red. Kind things are red. If Charlie is big and Charlie is red then Charlie is cold. Green things are quiet.
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is red.
("Harry" "is" "red" "+")
Kind things are red.
((("something" "is" "kind" "+")) -> ("something" "is" "red" "+"))
If Charlie is big and Charlie is red then Charlie is cold.
((("Charlie" "is" "big" "+") ("Charlie" "is" "red" "+")) -> ("Charlie" "is" "cold" "+"))
Green things are quiet.
((("something" "is" "green" "+")) -> ("something" "is" "quiet" "+"))
Harry is green.
True
1
proof
[(triple11)]
("Harry" "is" "green" "+")
triple11
Harry is not blue.
False
1
inv-proof
[(triple9)]
("Harry" "is" "blue" "-")
triple9
@0: Charlie is big.[(triple1)] Charlie is blue.[(triple2)] Charlie is cold.[(triple3 OR ((triple1 triple7) -> rule2) OR ((triple1 ((triple5) -> rule1)) -> rule2))] Charlie is green.[(triple4)] Charlie is kind.[(triple5)] Charlie is quiet.[(triple6 OR ((triple4) -> rule3))] Charlie is red.[(triple7 OR ((triple5) -> rule1))] Harry is big.[(triple8)] Harry is blue.[(triple9)] Harry is cold.[(triple10)] Harry is green.[(triple11)] Harry is kind.[(triple12)] Harry is quiet.[(triple13 OR ((triple11) -> rule3))] Harry is red.[(triple14 OR ((triple12) -> rule1))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
Charlie is blue.
("Charlie" "is" "blue" "+")
triple2
Charlie is cold.
("Charlie" "is" "cold" "+")
triple3
((triple1 triple7) -> (rule2 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
((triple1 ((triple5) -> (rule1 % int2))) -> (rule2 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
triple4
Charlie is kind.
("Charlie" "is" "kind" "+")
triple5
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple6
((triple4) -> (rule3 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
triple7
((triple5) -> (rule1 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
triple8
Harry is blue.
("Harry" "is" "blue" "+")
triple9
Harry is cold.
("Harry" "is" "cold" "+")
triple10
Harry is green.
("Harry" "is" "green" "+")
triple11
Harry is kind.
("Harry" "is" "kind" "+")
triple12
Harry is quiet.
("Harry" "is" "quiet" "+")
triple13
((triple11) -> (rule3 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
triple14
((triple12) -> (rule1 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1