Bob is blue. Bob is kind. Bob is nice. Bob is quiet. Bob is rough. Bob is white. Charlie is nice. Charlie is white. Erin is blue. Erin is green. Erin is kind. Erin is nice. Erin is quiet. Erin is rough. Erin is white. If someone is quiet and white then they are green. If someone is rough and green then they are white. Nice, white people are quiet. All blue, rough people are nice. All rough people are kind. If someone is quiet and nice then they are rough.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is white.
("Bob" "is" "white" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is white.
("Erin" "is" "white" "+")
If someone is quiet and white then they are green.
((("someone" "is" "quiet" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "green" "+"))
If someone is rough and green then they are white.
((("someone" "is" "rough" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "white" "+"))
Nice, white people are quiet.
((("someone" "is" "nice" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "quiet" "+"))
All blue, rough people are nice.
((("someone" "is" "blue" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "nice" "+"))
All rough people are kind.
((("someone" "is" "rough" "+")) -> ("someone" "is" "kind" "+"))
If someone is quiet and nice then they are rough.
((("someone" "is" "quiet" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "rough" "+"))
Bob is quiet.
True
1
proof
[(triple4 OR ((triple3 triple6) -> rule3) OR ((((triple1 triple5) -> rule4) triple6) -> rule3))]
("Bob" "is" "quiet" "+")
triple4
((triple3 triple6) -> (rule3 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
((((triple1 triple5) -> (rule4 % int2)) triple6) -> (rule3 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is not rough.
False
1
inv-proof
[(triple5 OR ((triple4 triple3) -> rule6) OR ((((triple3 triple6) -> rule3) triple3) -> rule6))]
("Bob" "is" "rough" "-")
triple5
((triple4 triple3) -> (rule6 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
((((triple3 triple6) -> (rule3 % int2)) triple3) -> (rule6 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is green.
True
3
proof
[(((triple4 triple6) -> rule1) OR ((((triple3 triple6) -> rule3) triple6) -> rule1) OR ((((((triple1 triple5) -> rule4) triple6) -> rule3) triple6) -> rule1))]
("Bob" "is" "green" "+")
((triple4 triple6) -> (rule1 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
((((triple3 triple6) -> (rule3 % int2)) triple6) -> (rule1 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
((((((triple1 triple5) -> (rule4 % int3)) triple6) -> (rule3 % int2)) triple6) -> (rule1 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
int3
Bob is not green.
False
3
inv-proof
[(((triple4 triple6) -> rule1) OR ((((triple3 triple6) -> rule3) triple6) -> rule1) OR ((((((triple1 triple5) -> rule4) triple6) -> rule3) triple6) -> rule1))]
("Bob" "is" "green" "-")
((triple4 triple6) -> (rule1 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
((((triple3 triple6) -> (rule3 % int2)) triple6) -> (rule1 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
((((((triple1 triple5) -> (rule4 % int3)) triple6) -> (rule3 % int2)) triple6) -> (rule1 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
int3
Charlie is green.
True
5
proof
[(((((triple7 triple8) -> rule3) triple8) -> rule1))]
("Charlie" "is" "green" "+")
((((triple7 triple8) -> (rule3 % int2)) triple8) -> (rule1 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is not green.
False
5
inv-proof
[(((((triple7 triple8) -> rule3) triple8) -> rule1))]
("Charlie" "is" "green" "-")
((((triple7 triple8) -> (rule3 % int2)) triple8) -> (rule1 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is kind.
True
6
proof
[(((((((triple7 triple8) -> rule3) triple7) -> rule6)) -> rule5))]
("Charlie" "is" "kind" "+")
((((((triple7 triple8) -> (rule3 % int3)) triple7) -> (rule6 % int2))) -> (rule5 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
Charlie is not kind.
False
6
inv-proof
[(((((((triple7 triple8) -> rule3) triple7) -> rule6)) -> rule5))]
("Charlie" "is" "kind" "-")
((((((triple7 triple8) -> (rule3 % int3)) triple7) -> (rule6 % int2))) -> (rule5 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
@0: Bob is blue.[(triple1)] Bob is kind.[(triple2 OR ((triple5) -> rule5) OR ((((triple4 triple3) -> rule6)) -> rule5) OR ((((((triple3 triple6) -> rule3) triple3) -> rule6)) -> rule5))] Bob is nice.[(triple3 OR ((triple1 triple5) -> rule4))] Bob is quiet.[(triple4 OR ((triple3 triple6) -> rule3) OR ((((triple1 triple5) -> rule4) triple6) -> rule3))] Bob is rough.[(triple5 OR ((triple4 triple3) -> rule6) OR ((((triple3 triple6) -> rule3) triple3) -> rule6))] Bob is white.[(triple6)] Charlie is nice.[(triple7)] Charlie is white.[(triple8)] Erin is blue.[(triple9)] Erin is green.[(triple10 OR ((triple13 triple15) -> rule1) OR ((((triple12 triple15) -> rule3) triple15) -> rule1) OR ((((((triple9 triple14) -> rule4) triple15) -> rule3) triple15) -> rule1))] Erin is kind.[(triple11 OR ((triple14) -> rule5) OR ((((triple13 triple12) -> rule6)) -> rule5) OR ((((((triple12 triple15) -> rule3) triple12) -> rule6)) -> rule5))] Erin is nice.[(triple12 OR ((triple9 triple14) -> rule4))] Erin is quiet.[(triple13 OR ((triple12 triple15) -> rule3) OR ((triple12 ((triple14 triple10) -> rule2)) -> rule3) OR ((((triple9 triple14) -> rule4) triple15) -> rule3) OR ((((triple9 triple14) -> rule4) ((triple14 triple10) -> rule2)) -> rule3))] Erin is rough.[(triple14 OR ((triple13 triple12) -> rule6) OR ((((triple12 triple15) -> rule3) triple12) -> rule6))] Erin is white.[(triple15 OR ((triple14 triple10) -> rule2) OR ((((triple13 triple12) -> rule6) triple10) -> rule2))] @1: Bob is green.[(((triple4 triple6) -> rule1) OR ((((triple3 triple6) -> rule3) triple6) -> rule1) OR ((((((triple1 triple5) -> rule4) triple6) -> rule3) triple6) -> rule1))] Charlie is quiet.[(((triple7 triple8) -> rule3))] @2: Charlie is green.[(((((triple7 triple8) -> rule3) triple8) -> rule1))] Charlie is rough.[(((((triple7 triple8) -> rule3) triple7) -> rule6))] @3: Charlie is kind.[(((((((triple7 triple8) -> rule3) triple7) -> rule6)) -> rule5))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Bob is kind.
("Bob" "is" "kind" "+")
triple2
((triple5) -> (rule5 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
((((triple4 triple3) -> (rule6 % int2))) -> (rule5 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
((((((triple3 triple6) -> (rule3 % int3)) triple3) -> (rule6 % int2))) -> (rule5 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
Bob is nice.
("Bob" "is" "nice" "+")
triple3
((triple1 triple5) -> (rule4 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
triple4
((triple3 triple6) -> (rule3 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
((((triple1 triple5) -> (rule4 % int2)) triple6) -> (rule3 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
triple5
((triple4 triple3) -> (rule6 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
((((triple3 triple6) -> (rule3 % int2)) triple3) -> (rule6 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
triple6
Charlie is nice.
("Charlie" "is" "nice" "+")
triple7
Charlie is white.
("Charlie" "is" "white" "+")
triple8
Erin is blue.
("Erin" "is" "blue" "+")
triple9
Erin is green.
("Erin" "is" "green" "+")
triple10
((triple13 triple15) -> (rule1 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
((((triple12 triple15) -> (rule3 % int2)) triple15) -> (rule1 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
((((((triple9 triple14) -> (rule4 % int3)) triple15) -> (rule3 % int2)) triple15) -> (rule1 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
int3
Erin is kind.
("Erin" "is" "kind" "+")
triple11
((triple14) -> (rule5 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
((((triple13 triple12) -> (rule6 % int2))) -> (rule5 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
((((((triple12 triple15) -> (rule3 % int3)) triple12) -> (rule6 % int2))) -> (rule5 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
int3
Erin is nice.
("Erin" "is" "nice" "+")
triple12
((triple9 triple14) -> (rule4 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
triple13
((triple12 triple15) -> (rule3 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
((triple12 ((triple14 triple10) -> (rule2 % int2))) -> (rule3 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
((((triple9 triple14) -> (rule4 % int2)) triple15) -> (rule3 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
((((triple9 triple14) -> (rule4 % int3)) ((triple14 triple10) -> (rule2 % int2))) -> (rule3 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
int3
Erin is rough.
("Erin" "is" "rough" "+")
triple14
((triple13 triple12) -> (rule6 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
((((triple12 triple15) -> (rule3 % int2)) triple12) -> (rule6 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
triple15
((triple14 triple10) -> (rule2 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
((((triple13 triple12) -> (rule6 % int2)) triple10) -> (rule2 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
((triple4 triple6) -> (rule1 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
((((triple3 triple6) -> (rule3 % int2)) triple6) -> (rule1 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
((((((triple1 triple5) -> (rule4 % int3)) triple6) -> (rule3 % int2)) triple6) -> (rule1 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
int3
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((triple7 triple8) -> (rule3 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
((((triple7 triple8) -> (rule3 % int2)) triple8) -> (rule1 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
((((triple7 triple8) -> (rule3 % int2)) triple7) -> (rule6 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
((((((triple7 triple8) -> (rule3 % int3)) triple7) -> (rule6 % int2))) -> (rule5 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3