Gary is blue. Gary is cold. Gary is not kind. Gary is red. Gary is rough. Gary is round. Gary is young. Red things are round. If something is kind then it is not rough. Blue things are not kind. Rough things are blue. If something is kind and not round then it is blue. All round things are blue. If something is young and not red then it is blue. If something is kind and not blue then it is cold.
Gary is blue.
("Gary" "is" "blue" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is not kind.
("Gary" "is" "kind" "-")
Gary is red.
("Gary" "is" "red" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is round.
("Gary" "is" "round" "+")
Gary is young.
("Gary" "is" "young" "+")
Red things are round.
((("something" "is" "red" "+")) -> ("something" "is" "round" "+"))
If something is kind then it is not rough.
((("something" "is" "kind" "+")) -> ("something" "is" "rough" "-"))
Blue things are not kind.
((("something" "is" "blue" "+")) -> ("something" "is" "kind" "-"))
Rough things are blue.
((("something" "is" "rough" "+")) -> ("something" "is" "blue" "+"))
If something is kind and not round then it is blue.
((("something" "is" "kind" "+") ("something" "is" "round" "~")) -> ("something" "is" "blue" "+"))
All round things are blue.
((("something" "is" "round" "+")) -> ("something" "is" "blue" "+"))
If something is young and not red then it is blue.
((("something" "is" "young" "+") ("something" "is" "red" "~")) -> ("something" "is" "blue" "+"))
If something is kind and not blue then it is cold.
((("something" "is" "kind" "+") ("something" "is" "blue" "~")) -> ("something" "is" "cold" "+"))
Gary is blue.
True
1
proof
[(triple1 OR ((triple5) -> rule4) OR ((triple6) -> rule6) OR ((((triple4) -> rule1)) -> rule6))]
("Gary" "is" "blue" "+")
triple1
((triple5) -> (rule4 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
((triple6) -> (rule6 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
((((triple4) -> (rule1 % int2))) -> (rule6 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is kind.
False
1
inv-proof
[(triple3 OR ((triple1) -> rule3) OR ((((triple5) -> rule4)) -> rule3) OR ((((triple6) -> rule6)) -> rule3) OR ((((((triple4) -> rule1)) -> rule6)) -> rule3))]
("Gary" "is" "kind" "+")
triple3
((triple1) -> (rule3 % int1))
Gary is not kind.
("Gary" "is" "kind" "-")
int1
((((triple5) -> (rule4 % int2))) -> (rule3 % int1))
Gary is not kind.
("Gary" "is" "kind" "-")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
((((triple6) -> (rule6 % int2))) -> (rule3 % int1))
Gary is not kind.
("Gary" "is" "kind" "-")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
((((((triple4) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Gary is not kind.
("Gary" "is" "kind" "-")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
@0: Gary is blue.[(triple1 OR ((triple5) -> rule4) OR ((triple6) -> rule6) OR ((((triple4) -> rule1)) -> rule6))] Gary is cold.[(triple2)] Gary is not kind.[(triple3 OR ((triple1) -> rule3) OR ((((triple5) -> rule4)) -> rule3) OR ((((triple6) -> rule6)) -> rule3) OR ((((((triple4) -> rule1)) -> rule6)) -> rule3))] Gary is red.[(triple4)] Gary is rough.[(triple5)] Gary is round.[(triple6 OR ((triple4) -> rule1))] Gary is young.[(triple7)]
Gary is blue.
("Gary" "is" "blue" "+")
triple1
((triple5) -> (rule4 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
((triple6) -> (rule6 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
((((triple4) -> (rule1 % int2))) -> (rule6 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
triple2
Gary is not kind.
("Gary" "is" "kind" "-")
triple3
((triple1) -> (rule3 % int1))
Gary is not kind.
("Gary" "is" "kind" "-")
int1
((((triple5) -> (rule4 % int2))) -> (rule3 % int1))
Gary is not kind.
("Gary" "is" "kind" "-")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
((((triple6) -> (rule6 % int2))) -> (rule3 % int1))
Gary is not kind.
("Gary" "is" "kind" "-")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
((((((triple4) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Gary is not kind.
("Gary" "is" "kind" "-")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
Gary is red.
("Gary" "is" "red" "+")
triple4
Gary is rough.
("Gary" "is" "rough" "+")
triple5
Gary is round.
("Gary" "is" "round" "+")
triple6
((triple4) -> (rule1 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
triple7