Dave is nice. Dave is round. Dave is white. Smart people are quiet. Round people are white. All round, rough people are kind. If someone is white and nice then they are rough. If Dave is nice then Dave is smart. All quiet people are rough.
Dave is nice.
("Dave" "is" "nice" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is white.
("Dave" "is" "white" "+")
Smart people are quiet.
((("someone" "is" "smart" "+")) -> ("someone" "is" "quiet" "+"))
Round people are white.
((("someone" "is" "round" "+")) -> ("someone" "is" "white" "+"))
All round, rough people are kind.
((("someone" "is" "round" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "kind" "+"))
If someone is white and nice then they are rough.
((("someone" "is" "white" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "rough" "+"))
If Dave is nice then Dave is smart.
((("Dave" "is" "nice" "+")) -> ("Dave" "is" "smart" "+"))
All quiet people are rough.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "rough" "+"))
Dave is white.
True
1
proof
[(triple3 OR ((triple2) -> rule2))]
("Dave" "is" "white" "+")
triple3
((triple2) -> (rule2 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is not white.
False
1
inv-proof
[(triple3 OR ((triple2) -> rule2))]
("Dave" "is" "white" "-")
triple3
((triple2) -> (rule2 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is smart.
True
2
proof
[(((triple1) -> rule5))]
("Dave" "is" "smart" "+")
((triple1) -> (rule5 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is not rough.
False
3
inv-proof
[(((triple3 triple1) -> rule4) OR ((((triple2) -> rule2) triple1) -> rule4) OR ((((((triple1) -> rule5)) -> rule1)) -> rule6))]
("Dave" "is" "rough" "-")
((triple3 triple1) -> (rule4 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
((((triple2) -> (rule2 % int2)) triple1) -> (rule4 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
((((((triple1) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
Dave is kind.
True
5
proof
[(((triple2 ((triple3 triple1) -> rule4)) -> rule3) OR ((triple2 ((((triple2) -> rule2) triple1) -> rule4)) -> rule3) OR ((triple2 ((((((triple1) -> rule5)) -> rule1)) -> rule6)) -> rule3))]
("Dave" "is" "kind" "+")
((triple2 ((triple3 triple1) -> (rule4 % int2))) -> (rule3 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
((triple2 ((((triple2) -> (rule2 % int3)) triple1) -> (rule4 % int2))) -> (rule3 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
((triple2 ((((((triple1) -> (rule5 % int4))) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
Dave is smart.
("Dave" "is" "smart" "+")
int4
Dave is not quiet.
False
3
inv-proof
[(((((triple1) -> rule5)) -> rule1))]
("Dave" "is" "quiet" "-")
((((triple1) -> (rule5 % int2))) -> (rule1 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
@0: Dave is nice.[(triple1)] Dave is round.[(triple2)] Dave is white.[(triple3 OR ((triple2) -> rule2))] @1: Dave is rough.[(((triple3 triple1) -> rule4) OR ((((triple2) -> rule2) triple1) -> rule4) OR ((((((triple1) -> rule5)) -> rule1)) -> rule6))] Dave is smart.[(((triple1) -> rule5))] @2: Dave is kind.[(((triple2 ((triple3 triple1) -> rule4)) -> rule3) OR ((triple2 ((((triple2) -> rule2) triple1) -> rule4)) -> rule3) OR ((triple2 ((((((triple1) -> rule5)) -> rule1)) -> rule6)) -> rule3))] Dave is quiet.[(((((triple1) -> rule5)) -> rule1))]
Dave is nice.
("Dave" "is" "nice" "+")
triple1
Dave is round.
("Dave" "is" "round" "+")
triple2
Dave is white.
("Dave" "is" "white" "+")
triple3
((triple2) -> (rule2 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
((triple3 triple1) -> (rule4 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
((((triple2) -> (rule2 % int2)) triple1) -> (rule4 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
((((((triple1) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
Dave is smart.
("Dave" "is" "smart" "+")
((triple1) -> (rule5 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
((triple2 ((triple3 triple1) -> (rule4 % int2))) -> (rule3 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
((triple2 ((((triple2) -> (rule2 % int3)) triple1) -> (rule4 % int2))) -> (rule3 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
((triple2 ((((((triple1) -> (rule5 % int4))) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
Dave is smart.
("Dave" "is" "smart" "+")
int4
Dave is quiet.
("Dave" "is" "quiet" "+")
((((triple1) -> (rule5 % int2))) -> (rule1 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2