Gary is kind. Gary is red. Gary is white. If someone is young and kind then they are rough. Nice people are rough. All young, kind people are rough. Kind people are white. Quiet people are nice. All quiet, rough people are kind. If Gary is white then Gary is quiet. If Gary is rough and Gary is young then Gary is kind.
Gary is kind.
("Gary" "is" "kind" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is white.
("Gary" "is" "white" "+")
If someone is young and kind then they are rough.
((("someone" "is" "young" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "rough" "+"))
Nice people are rough.
((("someone" "is" "nice" "+")) -> ("someone" "is" "rough" "+"))
All young, kind people are rough.
((("someone" "is" "young" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "rough" "+"))
Kind people are white.
((("someone" "is" "kind" "+")) -> ("someone" "is" "white" "+"))
Quiet people are nice.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "nice" "+"))
All quiet, rough people are kind.
((("someone" "is" "quiet" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "kind" "+"))
If Gary is white then Gary is quiet.
((("Gary" "is" "white" "+")) -> ("Gary" "is" "quiet" "+"))
If Gary is rough and Gary is young then Gary is kind.
((("Gary" "is" "rough" "+") ("Gary" "is" "young" "+")) -> ("Gary" "is" "kind" "+"))
Gary is kind.
True
1
proof
[(triple1 OR ((((triple3) -> rule7) ((((((triple3) -> rule7)) -> rule5)) -> rule2)) -> rule6))]
("Gary" "is" "kind" "+")
triple1
((((triple3) -> (rule7 % int4)) ((((((triple3) -> (rule7 % int4))) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3
Gary is quiet.
("Gary" "is" "quiet" "+")
int4
Gary is not kind.
False
1
inv-proof
[(triple1 OR ((((triple3) -> rule7) ((((((triple3) -> rule7)) -> rule5)) -> rule2)) -> rule6))]
("Gary" "is" "kind" "-")
triple1
((((triple3) -> (rule7 % int4)) ((((((triple3) -> (rule7 % int4))) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3
Gary is quiet.
("Gary" "is" "quiet" "+")
int4
Gary is quiet.
True
2
proof
[(((triple3) -> rule7) OR ((((triple1) -> rule4)) -> rule7))]
("Gary" "is" "quiet" "+")
((triple3) -> (rule7 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
((((triple1) -> (rule4 % int2))) -> (rule7 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is not quiet.
False
2
inv-proof
[(((triple3) -> rule7) OR ((((triple1) -> rule4)) -> rule7))]
("Gary" "is" "quiet" "-")
((triple3) -> (rule7 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
((((triple1) -> (rule4 % int2))) -> (rule7 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is nice.
True
3
proof
[(((((triple3) -> rule7)) -> rule5) OR ((((((triple1) -> rule4)) -> rule7)) -> rule5))]
("Gary" "is" "nice" "+")
((((triple3) -> (rule7 % int2))) -> (rule5 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
((((((triple1) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
Gary is not nice.
False
3
inv-proof
[(((((triple3) -> rule7)) -> rule5) OR ((((((triple1) -> rule4)) -> rule7)) -> rule5))]
("Gary" "is" "nice" "-")
((((triple3) -> (rule7 % int2))) -> (rule5 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
((((((triple1) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
@0: Gary is kind.[(triple1 OR ((((triple3) -> rule7) ((((((triple3) -> rule7)) -> rule5)) -> rule2)) -> rule6))] Gary is red.[(triple2)] Gary is white.[(triple3 OR ((triple1) -> rule4))] @1: Gary is quiet.[(((triple3) -> rule7) OR ((((triple1) -> rule4)) -> rule7))] @2: Gary is nice.[(((((triple3) -> rule7)) -> rule5) OR ((((((triple1) -> rule4)) -> rule7)) -> rule5))] @3: Gary is rough.[(((((((triple3) -> rule7)) -> rule5)) -> rule2) OR ((((((((triple1) -> rule4)) -> rule7)) -> rule5)) -> rule2))]
Gary is kind.
("Gary" "is" "kind" "+")
triple1
((((triple3) -> (rule7 % int4)) ((((((triple3) -> (rule7 % int4))) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3
Gary is quiet.
("Gary" "is" "quiet" "+")
int4
Gary is red.
("Gary" "is" "red" "+")
triple2
Gary is white.
("Gary" "is" "white" "+")
triple3
((triple1) -> (rule4 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
((triple3) -> (rule7 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
((((triple1) -> (rule4 % int2))) -> (rule7 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
((((triple3) -> (rule7 % int2))) -> (rule5 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
((((((triple1) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
Gary is rough.
("Gary" "is" "rough" "+")
((((((triple3) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
((((((((triple1) -> (rule4 % int4))) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
Gary is white.
("Gary" "is" "white" "+")
int4