Bob is nice. Bob is quiet. Bob is smart. All young, smart people are not rough. All kind people are young. If Bob is smart and Bob is quiet then Bob is kind. If Bob is nice and Bob is not smart then Bob is kind. All rough people are kind. All smart people are quiet.
Bob is nice.
("Bob" "is" "nice" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is smart.
("Bob" "is" "smart" "+")
All young, smart people are not rough.
((("someone" "is" "young" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "rough" "-"))
All kind people are young.
((("someone" "is" "kind" "+")) -> ("someone" "is" "young" "+"))
If Bob is smart and Bob is quiet then Bob is kind.
((("Bob" "is" "smart" "+") ("Bob" "is" "quiet" "+")) -> ("Bob" "is" "kind" "+"))
If Bob is nice and Bob is not smart then Bob is kind.
((("Bob" "is" "nice" "+") ("Bob" "is" "smart" "~")) -> ("Bob" "is" "kind" "+"))
All rough people are kind.
((("someone" "is" "rough" "+")) -> ("someone" "is" "kind" "+"))
All smart people are quiet.
((("someone" "is" "smart" "+")) -> ("someone" "is" "quiet" "+"))
Bob is smart.
True
1
proof
[(triple3)]
("Bob" "is" "smart" "+")
triple3
Bob is not quiet.
False
1
inv-proof
[(triple2 OR ((triple3) -> rule6))]
("Bob" "is" "quiet" "-")
triple2
((triple3) -> (rule6 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is kind.
True
3
proof
[(((triple3 triple2) -> rule3) OR ((triple3 ((triple3) -> rule6)) -> rule3))]
("Bob" "is" "kind" "+")
((triple3 triple2) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
((triple3 ((triple3) -> (rule6 % int2))) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is not kind.
False
3
inv-proof
[(((triple3 triple2) -> rule3) OR ((triple3 ((triple3) -> rule6)) -> rule3))]
("Bob" "is" "kind" "-")
((triple3 triple2) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
((triple3 ((triple3) -> (rule6 % int2))) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is young.
True
4
proof
[(((((triple3 triple2) -> rule3)) -> rule2) OR ((((triple3 ((triple3) -> rule6)) -> rule3)) -> rule2))]
("Bob" "is" "young" "+")
((((triple3 triple2) -> (rule3 % int2))) -> (rule2 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
((((triple3 ((triple3) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
Bob is not young.
False
4
inv-proof
[(((((triple3 triple2) -> rule3)) -> rule2) OR ((((triple3 ((triple3) -> rule6)) -> rule3)) -> rule2))]
("Bob" "is" "young" "-")
((((triple3 triple2) -> (rule3 % int2))) -> (rule2 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
((((triple3 ((triple3) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
Bob is not rough.
True
6
proof
[(((((((triple3 triple2) -> rule3)) -> rule2) triple3) -> rule1) OR ((((((triple3 ((triple3) -> rule6)) -> rule3)) -> rule2) triple3) -> rule1))]
("Bob" "is" "rough" "-")
((((((triple3 triple2) -> (rule3 % int3))) -> (rule2 % int2)) triple3) -> (rule1 % int1))
Bob is not rough.
("Bob" "is" "rough" "-")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
((((((triple3 ((triple3) -> (rule6 % int4))) -> (rule3 % int3))) -> (rule2 % int2)) triple3) -> (rule1 % int1))
Bob is not rough.
("Bob" "is" "rough" "-")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
Bob is quiet.
("Bob" "is" "quiet" "+")
int4
Bob is rough.
False
6
inv-proof
[(((((((triple3 triple2) -> rule3)) -> rule2) triple3) -> rule1) OR ((((((triple3 ((triple3) -> rule6)) -> rule3)) -> rule2) triple3) -> rule1))]
("Bob" "is" "rough" "+")
((((((triple3 triple2) -> (rule3 % int3))) -> (rule2 % int2)) triple3) -> (rule1 % int1))
Bob is not rough.
("Bob" "is" "rough" "-")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
((((((triple3 ((triple3) -> (rule6 % int4))) -> (rule3 % int3))) -> (rule2 % int2)) triple3) -> (rule1 % int1))
Bob is not rough.
("Bob" "is" "rough" "-")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
Bob is quiet.
("Bob" "is" "quiet" "+")
int4
@0: Bob is nice.[(triple1)] Bob is quiet.[(triple2 OR ((triple3) -> rule6))] Bob is smart.[(triple3)] @1: Bob is kind.[(((triple3 triple2) -> rule3) OR ((triple3 ((triple3) -> rule6)) -> rule3))] @2: Bob is young.[(((((triple3 triple2) -> rule3)) -> rule2) OR ((((triple3 ((triple3) -> rule6)) -> rule3)) -> rule2))] @3: Bob is not rough.[(((((((triple3 triple2) -> rule3)) -> rule2) triple3) -> rule1) OR ((((((triple3 ((triple3) -> rule6)) -> rule3)) -> rule2) triple3) -> rule1))]
Bob is nice.
("Bob" "is" "nice" "+")
triple1
Bob is quiet.
("Bob" "is" "quiet" "+")
triple2
((triple3) -> (rule6 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
triple3
Bob is kind.
("Bob" "is" "kind" "+")
((triple3 triple2) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
((triple3 ((triple3) -> (rule6 % int2))) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
((((triple3 triple2) -> (rule3 % int2))) -> (rule2 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
((((triple3 ((triple3) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
Bob is not rough.
("Bob" "is" "rough" "-")
((((((triple3 triple2) -> (rule3 % int3))) -> (rule2 % int2)) triple3) -> (rule1 % int1))
Bob is not rough.
("Bob" "is" "rough" "-")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
((((((triple3 ((triple3) -> (rule6 % int4))) -> (rule3 % int3))) -> (rule2 % int2)) triple3) -> (rule1 % int1))
Bob is not rough.
("Bob" "is" "rough" "-")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
Bob is quiet.
("Bob" "is" "quiet" "+")
int4