Charlie is blue. Charlie is cold. Charlie is green. Charlie is not kind. Charlie is rough. Harry is big. Harry is blue. Harry is cold. Harry is green. Harry is not kind. Harry is rough. Harry is smart. If something is kind then it is rough. If Charlie is cold then Charlie is big. If something is cold and green then it is smart. Cold things are smart. Green things are not kind. If something is smart and rough then it is cold.
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is not kind.
("Charlie" "is" "kind" "-")
Charlie is rough.
("Charlie" "is" "rough" "+")
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 not kind.
("Harry" "is" "kind" "-")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is smart.
("Harry" "is" "smart" "+")
If something is kind then it is rough.
((("something" "is" "kind" "+")) -> ("something" "is" "rough" "+"))
If Charlie is cold then Charlie is big.
((("Charlie" "is" "cold" "+")) -> ("Charlie" "is" "big" "+"))
If something is cold and green then it is smart.
((("something" "is" "cold" "+") ("something" "is" "green" "+")) -> ("something" "is" "smart" "+"))
Cold things are smart.
((("something" "is" "cold" "+")) -> ("something" "is" "smart" "+"))
Green things are not kind.
((("something" "is" "green" "+")) -> ("something" "is" "kind" "-"))
If something is smart and rough then it is cold.
((("something" "is" "smart" "+") ("something" "is" "rough" "+")) -> ("something" "is" "cold" "+"))
Harry is green.
True
1
proof
[(triple9)]
("Harry" "is" "green" "+")
triple9
Charlie is not blue.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "blue" "-")
triple1
Charlie is smart.
True
2
proof
[(((triple2) -> rule4) OR ((triple2 triple3) -> rule3))]
("Charlie" "is" "smart" "+")
((triple2) -> (rule4 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
((triple2 triple3) -> (rule3 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is not smart.
False
2
inv-proof
[(((triple2) -> rule4) OR ((triple2 triple3) -> rule3))]
("Charlie" "is" "smart" "-")
((triple2) -> (rule4 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
((triple2 triple3) -> (rule3 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
@0: Charlie is blue.[(triple1)] Charlie is cold.[(triple2)] Charlie is green.[(triple3)] Charlie is not kind.[(triple4 OR ((triple3) -> rule5))] Charlie is rough.[(triple5)] Harry is big.[(triple6)] Harry is blue.[(triple7)] Harry is cold.[(triple8 OR ((triple12 triple11) -> rule6))] Harry is green.[(triple9)] Harry is not kind.[(triple10 OR ((triple9) -> rule5))] Harry is rough.[(triple11)] Harry is smart.[(triple12 OR ((triple8) -> rule4) OR ((triple8 triple9) -> rule3))] @1: Charlie is big.[(((triple2) -> rule2))] Charlie is smart.[(((triple2) -> rule4) OR ((triple2 triple3) -> rule3))]
Charlie is blue.
("Charlie" "is" "blue" "+")
triple1
Charlie is cold.
("Charlie" "is" "cold" "+")
triple2
Charlie is green.
("Charlie" "is" "green" "+")
triple3
Charlie is not kind.
("Charlie" "is" "kind" "-")
triple4
((triple3) -> (rule5 % int1))
Charlie is not kind.
("Charlie" "is" "kind" "-")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
triple5
Harry is big.
("Harry" "is" "big" "+")
triple6
Harry is blue.
("Harry" "is" "blue" "+")
triple7
Harry is cold.
("Harry" "is" "cold" "+")
triple8
((triple12 triple11) -> (rule6 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
triple9
Harry is not kind.
("Harry" "is" "kind" "-")
triple10
((triple9) -> (rule5 % int1))
Harry is not kind.
("Harry" "is" "kind" "-")
int1
Harry is rough.
("Harry" "is" "rough" "+")
triple11
Harry is smart.
("Harry" "is" "smart" "+")
triple12
((triple8) -> (rule4 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
((triple8 triple9) -> (rule3 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
((triple2) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
((triple2) -> (rule4 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
((triple2 triple3) -> (rule3 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1