Bob is not blue. Bob is green. Bob is kind. Bob is nice. Bob is rough. Bob is round. Bob is smart. If someone is nice and smart then they are rough. If Bob is blue and Bob is not nice then Bob is not kind. If Bob is kind and Bob is nice then Bob is green. Smart, rough people are kind. If someone is blue and not nice then they are green. Rough, green people are smart. If someone is green then they are round. If someone is rough and not green then they are round.
Bob is not blue.
("Bob" "is" "blue" "-")
Bob is green.
("Bob" "is" "green" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is smart.
("Bob" "is" "smart" "+")
If someone is nice and smart then they are rough.
((("someone" "is" "nice" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "rough" "+"))
If Bob is blue and Bob is not nice then Bob is not kind.
((("Bob" "is" "blue" "+") ("Bob" "is" "nice" "~")) -> ("Bob" "is" "kind" "-"))
If Bob is kind and Bob is nice then Bob is green.
((("Bob" "is" "kind" "+") ("Bob" "is" "nice" "+")) -> ("Bob" "is" "green" "+"))
Smart, rough people are kind.
((("someone" "is" "smart" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "kind" "+"))
If someone is blue and not nice then they are green.
((("someone" "is" "blue" "+") ("someone" "is" "nice" "~")) -> ("someone" "is" "green" "+"))
Rough, green people are smart.
((("someone" "is" "rough" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "smart" "+"))
If someone is green then they are round.
((("someone" "is" "green" "+")) -> ("someone" "is" "round" "+"))
If someone is rough and not green then they are round.
((("someone" "is" "rough" "+") ("someone" "is" "green" "~")) -> ("someone" "is" "round" "+"))
Bob is nice.
True
1
proof
[(triple4)]
("Bob" "is" "nice" "+")
triple4
Bob is not kind.
False
1
inv-proof
[(triple3 OR ((triple7 triple5) -> rule4) OR ((triple7 ((triple4 triple7) -> rule1)) -> rule4) OR ((((triple5 triple2) -> rule6) triple5) -> rule4) OR ((((triple5 triple2) -> rule6) ((triple4 triple7) -> rule1)) -> rule4))]
("Bob" "is" "kind" "-")
triple3
((triple7 triple5) -> (rule4 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
((triple7 ((triple4 triple7) -> (rule1 % int2))) -> (rule4 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
((((triple5 triple2) -> (rule6 % int2)) triple5) -> (rule4 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
((((triple5 triple2) -> (rule6 % int3)) ((triple4 triple7) -> (rule1 % int2))) -> (rule4 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
@0: Bob is green.[(triple2 OR ((triple3 triple4) -> rule3) OR ((((triple7 triple5) -> rule4) triple4) -> rule3) OR ((((triple7 ((triple4 triple7) -> rule1)) -> rule4) triple4) -> rule3))] Bob is kind.[(triple3 OR ((triple7 triple5) -> rule4) OR ((triple7 ((triple4 triple7) -> rule1)) -> rule4) OR ((((triple5 triple2) -> rule6) triple5) -> rule4) OR ((((triple5 triple2) -> rule6) ((triple4 triple7) -> rule1)) -> rule4))] Bob is nice.[(triple4)] Bob is not blue.[(triple1)] Bob is rough.[(triple5 OR ((triple4 triple7) -> rule1))] Bob is round.[(triple6 OR ((triple2) -> rule7) OR ((((triple3 triple4) -> rule3)) -> rule7) OR ((((((triple7 triple5) -> rule4) triple4) -> rule3)) -> rule7) OR ((((((triple7 ((triple4 triple7) -> rule1)) -> rule4) triple4) -> rule3)) -> rule7))] Bob is smart.[(triple7 OR ((triple5 triple2) -> rule6) OR ((triple5 ((triple3 triple4) -> rule3)) -> rule6))]
Bob is green.
("Bob" "is" "green" "+")
triple2
((triple3 triple4) -> (rule3 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
((((triple7 triple5) -> (rule4 % int2)) triple4) -> (rule3 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
((((triple7 ((triple4 triple7) -> (rule1 % int3))) -> (rule4 % int2)) triple4) -> (rule3 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
Bob is kind.
("Bob" "is" "kind" "+")
triple3
((triple7 triple5) -> (rule4 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
((triple7 ((triple4 triple7) -> (rule1 % int2))) -> (rule4 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
((((triple5 triple2) -> (rule6 % int2)) triple5) -> (rule4 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
((((triple5 triple2) -> (rule6 % int3)) ((triple4 triple7) -> (rule1 % int2))) -> (rule4 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
Bob is nice.
("Bob" "is" "nice" "+")
triple4
Bob is not blue.
("Bob" "is" "blue" "-")
triple1
Bob is rough.
("Bob" "is" "rough" "+")
triple5
((triple4 triple7) -> (rule1 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
triple6
((triple2) -> (rule7 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
((((triple3 triple4) -> (rule3 % int2))) -> (rule7 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
((((((triple7 triple5) -> (rule4 % int3)) triple4) -> (rule3 % int2))) -> (rule7 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
((((((triple7 ((triple4 triple7) -> (rule1 % int4))) -> (rule4 % int3)) triple4) -> (rule3 % int2))) -> (rule7 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
Bob is rough.
("Bob" "is" "rough" "+")
int4
Bob is smart.
("Bob" "is" "smart" "+")
triple7
((triple5 triple2) -> (rule6 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
((triple5 ((triple3 triple4) -> (rule3 % int2))) -> (rule6 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2