Gary is cold. Gary is round. Gary is smart. If Gary is rough and Gary is round then Gary is red. If someone is red then they are cold. All red people are kind. If Gary is round and Gary is cold then Gary is kind. If someone is kind then they are white. If someone is white and cold then they are red. Red people are round. If someone is smart then they are cold.
Gary is cold.
("Gary" "is" "cold" "+")
Gary is round.
("Gary" "is" "round" "+")
Gary is smart.
("Gary" "is" "smart" "+")
If Gary is rough and Gary is round then Gary is red.
((("Gary" "is" "rough" "+") ("Gary" "is" "round" "+")) -> ("Gary" "is" "red" "+"))
If someone is red then they are cold.
((("someone" "is" "red" "+")) -> ("someone" "is" "cold" "+"))
All red people are kind.
((("someone" "is" "red" "+")) -> ("someone" "is" "kind" "+"))
If Gary is round and Gary is cold then Gary is kind.
((("Gary" "is" "round" "+") ("Gary" "is" "cold" "+")) -> ("Gary" "is" "kind" "+"))
If someone is kind then they are white.
((("someone" "is" "kind" "+")) -> ("someone" "is" "white" "+"))
If someone is white and cold then they are red.
((("someone" "is" "white" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "red" "+"))
Red people are round.
((("someone" "is" "red" "+")) -> ("someone" "is" "round" "+"))
If someone is smart then they are cold.
((("someone" "is" "smart" "+")) -> ("someone" "is" "cold" "+"))
Gary is cold.
True
1
proof
[(triple1 OR ((triple3) -> rule8))]
("Gary" "is" "cold" "+")
triple1
((triple3) -> (rule8 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is not smart.
False
1
inv-proof
[(triple3)]
("Gary" "is" "smart" "-")
triple3
Gary is kind.
True
3
proof
[(((triple2 triple1) -> rule4) OR ((triple2 ((triple3) -> rule8)) -> rule4))]
("Gary" "is" "kind" "+")
((triple2 triple1) -> (rule4 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
((triple2 ((triple3) -> (rule8 % int2))) -> (rule4 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is not kind.
False
3
inv-proof
[(((triple2 triple1) -> rule4) OR ((triple2 ((triple3) -> rule8)) -> rule4))]
("Gary" "is" "kind" "-")
((triple2 triple1) -> (rule4 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
((triple2 ((triple3) -> (rule8 % int2))) -> (rule4 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is white.
True
4
proof
[(((((triple2 triple1) -> rule4)) -> rule5) OR ((((triple2 ((triple3) -> rule8)) -> rule4)) -> rule5))]
("Gary" "is" "white" "+")
((((triple2 triple1) -> (rule4 % int2))) -> (rule5 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
((((triple2 ((triple3) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
Gary is not white.
False
4
inv-proof
[(((((triple2 triple1) -> rule4)) -> rule5) OR ((((triple2 ((triple3) -> rule8)) -> rule4)) -> rule5))]
("Gary" "is" "white" "-")
((((triple2 triple1) -> (rule4 % int2))) -> (rule5 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
((((triple2 ((triple3) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
Gary is red.
True
6
proof
[(((((((triple2 triple1) -> rule4)) -> rule5) triple1) -> rule6) OR ((((((triple2 triple1) -> rule4)) -> rule5) ((triple3) -> rule8)) -> rule6) OR ((((((triple2 ((triple3) -> rule8)) -> rule4)) -> rule5) triple1) -> rule6) OR ((((((triple2 ((triple3) -> rule8)) -> rule4)) -> rule5) ((triple3) -> rule8)) -> rule6))]
("Gary" "is" "red" "+")
((((((triple2 triple1) -> (rule4 % int3))) -> (rule5 % int2)) triple1) -> (rule6 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
int3
((((((triple2 triple1) -> (rule4 % int4))) -> (rule5 % int3)) ((triple3) -> (rule8 % int2))) -> (rule6 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
Gary is kind.
("Gary" "is" "kind" "+")
int4
((((((triple2 ((triple3) -> (rule8 % int4))) -> (rule4 % int3))) -> (rule5 % int2)) triple1) -> (rule6 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
int3
Gary is cold.
("Gary" "is" "cold" "+")
int4
((((((triple2 ((triple3) -> (rule8 % int4))) -> (rule4 % int3))) -> (rule5 % int2)) ((triple3) -> (rule8 % int4))) -> (rule6 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
int3
Gary is cold.
("Gary" "is" "cold" "+")
int4
Gary is not red.
False
6
inv-proof
[(((((((triple2 triple1) -> rule4)) -> rule5) triple1) -> rule6) OR ((((((triple2 triple1) -> rule4)) -> rule5) ((triple3) -> rule8)) -> rule6) OR ((((((triple2 ((triple3) -> rule8)) -> rule4)) -> rule5) triple1) -> rule6) OR ((((((triple2 ((triple3) -> rule8)) -> rule4)) -> rule5) ((triple3) -> rule8)) -> rule6))]
("Gary" "is" "red" "-")
((((((triple2 triple1) -> (rule4 % int3))) -> (rule5 % int2)) triple1) -> (rule6 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
int3
((((((triple2 triple1) -> (rule4 % int4))) -> (rule5 % int3)) ((triple3) -> (rule8 % int2))) -> (rule6 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
Gary is kind.
("Gary" "is" "kind" "+")
int4
((((((triple2 ((triple3) -> (rule8 % int4))) -> (rule4 % int3))) -> (rule5 % int2)) triple1) -> (rule6 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
int3
Gary is cold.
("Gary" "is" "cold" "+")
int4
((((((triple2 ((triple3) -> (rule8 % int4))) -> (rule4 % int3))) -> (rule5 % int2)) ((triple3) -> (rule8 % int4))) -> (rule6 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
int3
Gary is cold.
("Gary" "is" "cold" "+")
int4
@0: Gary is cold.[(triple1 OR ((triple3) -> rule8))] Gary is round.[(triple2)] Gary is smart.[(triple3)] @1: Gary is kind.[(((triple2 triple1) -> rule4) OR ((triple2 ((triple3) -> rule8)) -> rule4))] @2: Gary is white.[(((((triple2 triple1) -> rule4)) -> rule5) OR ((((triple2 ((triple3) -> rule8)) -> rule4)) -> rule5))] @3: Gary is red.[(((((((triple2 triple1) -> rule4)) -> rule5) triple1) -> rule6) OR ((((((triple2 triple1) -> rule4)) -> rule5) ((triple3) -> rule8)) -> rule6) OR ((((((triple2 ((triple3) -> rule8)) -> rule4)) -> rule5) triple1) -> rule6) OR ((((((triple2 ((triple3) -> rule8)) -> rule4)) -> rule5) ((triple3) -> rule8)) -> rule6))]
Gary is cold.
("Gary" "is" "cold" "+")
triple1
((triple3) -> (rule8 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
triple2
Gary is smart.
("Gary" "is" "smart" "+")
triple3
Gary is kind.
("Gary" "is" "kind" "+")
((triple2 triple1) -> (rule4 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
((triple2 ((triple3) -> (rule8 % int2))) -> (rule4 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
((((triple2 triple1) -> (rule4 % int2))) -> (rule5 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
((((triple2 ((triple3) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
Gary is red.
("Gary" "is" "red" "+")
((((((triple2 triple1) -> (rule4 % int3))) -> (rule5 % int2)) triple1) -> (rule6 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
int3
((((((triple2 triple1) -> (rule4 % int4))) -> (rule5 % int3)) ((triple3) -> (rule8 % int2))) -> (rule6 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
Gary is kind.
("Gary" "is" "kind" "+")
int4
((((((triple2 ((triple3) -> (rule8 % int4))) -> (rule4 % int3))) -> (rule5 % int2)) triple1) -> (rule6 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
int3
Gary is cold.
("Gary" "is" "cold" "+")
int4
((((((triple2 ((triple3) -> (rule8 % int4))) -> (rule4 % int3))) -> (rule5 % int2)) ((triple3) -> (rule8 % int4))) -> (rule6 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
int3
Gary is cold.
("Gary" "is" "cold" "+")
int4