Dave is kind. Dave is nice. Dave is quiet. Dave is red. Dave is rough. Dave is white. Dave is young. Erin is kind. Erin is nice. Erin is quiet. Erin is red. Erin is white. If something is quiet then it is red. If Dave is quiet and Dave is rough then Dave is nice. All young, quiet things are nice. Quiet things are rough. If something is white and nice then it is kind. If something is nice then it is kind.
Dave is kind.
("Dave" "is" "kind" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is white.
("Dave" "is" "white" "+")
Dave is young.
("Dave" "is" "young" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is white.
("Erin" "is" "white" "+")
If something is quiet then it is red.
((("something" "is" "quiet" "+")) -> ("something" "is" "red" "+"))
If Dave is quiet and Dave is rough then Dave is nice.
((("Dave" "is" "quiet" "+") ("Dave" "is" "rough" "+")) -> ("Dave" "is" "nice" "+"))
All young, quiet things are nice.
((("something" "is" "young" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "nice" "+"))
Quiet things are rough.
((("something" "is" "quiet" "+")) -> ("something" "is" "rough" "+"))
If something is white and nice then it is kind.
((("something" "is" "white" "+") ("something" "is" "nice" "+")) -> ("something" "is" "kind" "+"))
If something is nice then it is kind.
((("something" "is" "nice" "+")) -> ("something" "is" "kind" "+"))
Dave is quiet.
True
1
proof
[(triple3)]
("Dave" "is" "quiet" "+")
triple3
Erin is not red.
False
1
inv-proof
[(triple11 OR ((triple10) -> rule1))]
("Erin" "is" "red" "-")
triple11
((triple10) -> (rule1 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
@0: Dave is kind.[(triple1 OR ((triple2) -> rule6) OR ((triple6 triple2) -> rule5) OR ((((triple3 triple5) -> rule2)) -> rule6) OR ((((triple7 triple3) -> rule3)) -> rule6) OR ((triple6 ((triple3 triple5) -> rule2)) -> rule5) OR ((triple6 ((triple7 triple3) -> rule3)) -> rule5) OR ((((triple3 ((triple3) -> rule4)) -> rule2)) -> rule6) OR ((triple6 ((triple3 ((triple3) -> rule4)) -> rule2)) -> rule5))] Dave is nice.[(triple2 OR ((triple3 triple5) -> rule2) OR ((triple7 triple3) -> rule3) OR ((triple3 ((triple3) -> rule4)) -> rule2))] Dave is quiet.[(triple3)] Dave is red.[(triple4 OR ((triple3) -> rule1))] Dave is rough.[(triple5 OR ((triple3) -> rule4))] Dave is white.[(triple6)] Dave is young.[(triple7)] Erin is kind.[(triple8 OR ((triple9) -> rule6) OR ((triple12 triple9) -> rule5))] Erin is nice.[(triple9)] Erin is quiet.[(triple10)] Erin is red.[(triple11 OR ((triple10) -> rule1))] Erin is white.[(triple12)] @1: Erin is rough.[(((triple10) -> rule4))]
Dave is kind.
("Dave" "is" "kind" "+")
triple1
((triple2) -> (rule6 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
((triple6 triple2) -> (rule5 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
((((triple3 triple5) -> (rule2 % int2))) -> (rule6 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
((((triple7 triple3) -> (rule3 % int2))) -> (rule6 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
((triple6 ((triple3 triple5) -> (rule2 % int2))) -> (rule5 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
((triple6 ((triple7 triple3) -> (rule3 % int2))) -> (rule5 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
((((triple3 ((triple3) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
((triple6 ((triple3 ((triple3) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Dave is nice.
("Dave" "is" "nice" "+")
triple2
((triple3 triple5) -> (rule2 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
((triple7 triple3) -> (rule3 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
((triple3 ((triple3) -> (rule4 % int2))) -> (rule2 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
triple3
Dave is red.
("Dave" "is" "red" "+")
triple4
((triple3) -> (rule1 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
triple5
((triple3) -> (rule4 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
triple6
Dave is young.
("Dave" "is" "young" "+")
triple7
Erin is kind.
("Erin" "is" "kind" "+")
triple8
((triple9) -> (rule6 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
((triple12 triple9) -> (rule5 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
triple9
Erin is quiet.
("Erin" "is" "quiet" "+")
triple10
Erin is red.
("Erin" "is" "red" "+")
triple11
((triple10) -> (rule1 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
triple12
Erin is rough.
("Erin" "is" "rough" "+")
((triple10) -> (rule4 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1