Bob is not blue. Bob is nice. Bob is not rough. Bob is not smart. Bob is not white. Erin is big. Erin is blue. Erin is not nice. Erin is rough. Erin is smart. Erin is white. Erin is young. If something is rough then it is not nice. If something is blue then it is not nice. If Bob is nice then Bob is young. If something is big then it is rough. If something is rough then it is white. If Erin is rough and Erin is not nice then Erin is young.
Bob is not blue.
("Bob" "is" "blue" "-")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is not rough.
("Bob" "is" "rough" "-")
Bob is not smart.
("Bob" "is" "smart" "-")
Bob is not white.
("Bob" "is" "white" "-")
Erin is big.
("Erin" "is" "big" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is not nice.
("Erin" "is" "nice" "-")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Erin is white.
("Erin" "is" "white" "+")
Erin is young.
("Erin" "is" "young" "+")
If something is rough then it is not nice.
((("something" "is" "rough" "+")) -> ("something" "is" "nice" "-"))
If something is blue then it is not nice.
((("something" "is" "blue" "+")) -> ("something" "is" "nice" "-"))
If Bob is nice then Bob is young.
((("Bob" "is" "nice" "+")) -> ("Bob" "is" "young" "+"))
If something is big then it is rough.
((("something" "is" "big" "+")) -> ("something" "is" "rough" "+"))
If something is rough then it is white.
((("something" "is" "rough" "+")) -> ("something" "is" "white" "+"))
If Erin is rough and Erin is not nice then Erin is young.
((("Erin" "is" "rough" "+") ("Erin" "is" "nice" "~")) -> ("Erin" "is" "young" "+"))
Erin is smart.
True
1
proof
[(triple10)]
("Erin" "is" "smart" "+")
triple10
Bob is not nice.
False
1
inv-proof
[(triple2)]
("Bob" "is" "nice" "-")
triple2
Bob is young.
True
2
proof
[(((triple2) -> rule3))]
("Bob" "is" "young" "+")
((triple2) -> (rule3 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is not young.
False
2
inv-proof
[(((triple2) -> rule3))]
("Bob" "is" "young" "-")
((triple2) -> (rule3 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
@0: Bob is nice.[(triple2)] Bob is not blue.[(triple1)] Bob is not rough.[(triple3)] Bob is not smart.[(triple4)] Bob is not white.[(triple5)] Erin is big.[(triple6)] Erin is blue.[(triple7)] Erin is not nice.[(triple8 OR ((triple7) -> rule2) OR ((triple9) -> rule1) OR ((((triple6) -> rule4)) -> rule1))] Erin is rough.[(triple9 OR ((triple6) -> rule4))] Erin is smart.[(triple10)] Erin is white.[(triple11 OR ((triple9) -> rule5) OR ((((triple6) -> rule4)) -> rule5))] Erin is young.[(triple12 OR ((triple9 triple8) -> rule6) OR ((triple9 ((triple7) -> rule2)) -> rule6) OR ((triple9 ((triple9) -> rule1)) -> rule6) OR ((((triple6) -> rule4) triple8) -> rule6) OR ((((triple6) -> rule4) ((triple7) -> rule2)) -> rule6) OR ((((triple6) -> rule4) ((triple9) -> rule1)) -> rule6) OR ((triple9 ((((triple6) -> rule4)) -> rule1)) -> rule6) OR ((((triple6) -> rule4) ((((triple6) -> rule4)) -> rule1)) -> rule6))] @1: Bob is young.[(((triple2) -> rule3))]
Bob is nice.
("Bob" "is" "nice" "+")
triple2
Bob is not blue.
("Bob" "is" "blue" "-")
triple1
Bob is not rough.
("Bob" "is" "rough" "-")
triple3
Bob is not smart.
("Bob" "is" "smart" "-")
triple4
Bob is not white.
("Bob" "is" "white" "-")
triple5
Erin is big.
("Erin" "is" "big" "+")
triple6
Erin is blue.
("Erin" "is" "blue" "+")
triple7
Erin is not nice.
("Erin" "is" "nice" "-")
triple8
((triple7) -> (rule2 % int1))
Erin is not nice.
("Erin" "is" "nice" "-")
int1
((triple9) -> (rule1 % int1))
Erin is not nice.
("Erin" "is" "nice" "-")
int1
((((triple6) -> (rule4 % int2))) -> (rule1 % int1))
Erin is not nice.
("Erin" "is" "nice" "-")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
triple9
((triple6) -> (rule4 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
triple10
Erin is white.
("Erin" "is" "white" "+")
triple11
((triple9) -> (rule5 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
((((triple6) -> (rule4 % int2))) -> (rule5 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
triple12
((triple9 triple8) -> (rule6 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
((triple9 ((triple7) -> (rule2 % int2))) -> (rule6 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is not nice.
("Erin" "is" "nice" "-")
int2
((triple9 ((triple9) -> (rule1 % int2))) -> (rule6 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is not nice.
("Erin" "is" "nice" "-")
int2
((((triple6) -> (rule4 % int2)) triple8) -> (rule6 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
((((triple6) -> (rule4 % int3)) ((triple7) -> (rule2 % int2))) -> (rule6 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is not nice.
("Erin" "is" "nice" "-")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
((((triple6) -> (rule4 % int3)) ((triple9) -> (rule1 % int2))) -> (rule6 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is not nice.
("Erin" "is" "nice" "-")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
((triple9 ((((triple6) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is not nice.
("Erin" "is" "nice" "-")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
((((triple6) -> (rule4 % int3)) ((((triple6) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is not nice.
("Erin" "is" "nice" "-")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
Bob is young.
("Bob" "is" "young" "+")
((triple2) -> (rule3 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1