Charlie is big. Charlie is not cold. Charlie is green. Charlie is kind. Charlie is not quiet. Charlie is red. Charlie is rough. Gary is big. Gary is kind. Gary is not quiet. Gary is red. Gary is rough. All red things are rough. Cold things are red. If Charlie is not kind then Charlie is red. If Gary is kind and Gary is not big then Gary is quiet. If something is green then it is not cold. If something is red and not big then it is not cold. If something is rough and not kind then it is green. If Gary is rough then Gary is green.
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is not cold.
("Charlie" "is" "cold" "-")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is not quiet.
("Gary" "is" "quiet" "-")
Gary is red.
("Gary" "is" "red" "+")
Gary is rough.
("Gary" "is" "rough" "+")
All red things are rough.
((("something" "is" "red" "+")) -> ("something" "is" "rough" "+"))
Cold things are red.
((("something" "is" "cold" "+")) -> ("something" "is" "red" "+"))
If Charlie is not kind then Charlie is red.
((("Charlie" "is" "kind" "~")) -> ("Charlie" "is" "red" "+"))
If Gary is kind and Gary is not big then Gary is quiet.
((("Gary" "is" "kind" "+") ("Gary" "is" "big" "~")) -> ("Gary" "is" "quiet" "+"))
If something is green then it is not cold.
((("something" "is" "green" "+")) -> ("something" "is" "cold" "-"))
If something is red and not big then it is not cold.
((("something" "is" "red" "+") ("something" "is" "big" "~")) -> ("something" "is" "cold" "-"))
If something is rough and not kind then it is green.
((("something" "is" "rough" "+") ("something" "is" "kind" "~")) -> ("something" "is" "green" "+"))
If Gary is rough then Gary is green.
((("Gary" "is" "rough" "+")) -> ("Gary" "is" "green" "+"))
Charlie is red.
True
1
proof
[(triple6)]
("Charlie" "is" "red" "+")
triple6
Charlie is not green.
False
1
inv-proof
[(triple3)]
("Charlie" "is" "green" "-")
triple3
Gary is green.
True
2
proof
[(((triple12) -> rule8) OR ((((triple11) -> rule1)) -> rule8))]
("Gary" "is" "green" "+")
((triple12) -> (rule8 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
((((triple11) -> (rule1 % int2))) -> (rule8 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is not green.
False
2
inv-proof
[(((triple12) -> rule8) OR ((((triple11) -> rule1)) -> rule8))]
("Gary" "is" "green" "-")
((triple12) -> (rule8 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
((((triple11) -> (rule1 % int2))) -> (rule8 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is not cold.
True
3
proof
[(((((triple12) -> rule8)) -> rule5) OR ((((((triple11) -> rule1)) -> rule8)) -> rule5))]
("Gary" "is" "cold" "-")
((((triple12) -> (rule8 % int2))) -> (rule5 % int1))
Gary is not cold.
("Gary" "is" "cold" "-")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
((((((triple11) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule5 % int1))
Gary is not cold.
("Gary" "is" "cold" "-")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
Gary is cold.
False
3
inv-proof
[(((((triple12) -> rule8)) -> rule5) OR ((((((triple11) -> rule1)) -> rule8)) -> rule5))]
("Gary" "is" "cold" "+")
((((triple12) -> (rule8 % int2))) -> (rule5 % int1))
Gary is not cold.
("Gary" "is" "cold" "-")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
((((((triple11) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule5 % int1))
Gary is not cold.
("Gary" "is" "cold" "-")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
@0: Charlie is big.[(triple1)] Charlie is green.[(triple3)] Charlie is kind.[(triple4)] Charlie is not cold.[(triple2 OR ((triple3) -> rule5))] Charlie is not quiet.[(triple5)] Charlie is red.[(triple6)] Charlie is rough.[(triple7 OR ((triple6) -> rule1))] Gary is big.[(triple8)] Gary is kind.[(triple9)] Gary is not quiet.[(triple10)] Gary is red.[(triple11)] Gary is rough.[(triple12 OR ((triple11) -> rule1))] @1: Gary is green.[(((triple12) -> rule8) OR ((((triple11) -> rule1)) -> rule8))] @2: Gary is not cold.[(((((triple12) -> rule8)) -> rule5) OR ((((((triple11) -> rule1)) -> rule8)) -> rule5))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
Charlie is green.
("Charlie" "is" "green" "+")
triple3
Charlie is kind.
("Charlie" "is" "kind" "+")
triple4
Charlie is not cold.
("Charlie" "is" "cold" "-")
triple2
((triple3) -> (rule5 % int1))
Charlie is not cold.
("Charlie" "is" "cold" "-")
int1
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
triple5
Charlie is red.
("Charlie" "is" "red" "+")
triple6
Charlie is rough.
("Charlie" "is" "rough" "+")
triple7
((triple6) -> (rule1 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
triple8
Gary is kind.
("Gary" "is" "kind" "+")
triple9
Gary is not quiet.
("Gary" "is" "quiet" "-")
triple10
Gary is red.
("Gary" "is" "red" "+")
triple11
Gary is rough.
("Gary" "is" "rough" "+")
triple12
((triple11) -> (rule1 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
((triple12) -> (rule8 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
((((triple11) -> (rule1 % int2))) -> (rule8 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is not cold.
("Gary" "is" "cold" "-")
((((triple12) -> (rule8 % int2))) -> (rule5 % int1))
Gary is not cold.
("Gary" "is" "cold" "-")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
((((((triple11) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule5 % int1))
Gary is not cold.
("Gary" "is" "cold" "-")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3