Bob is big. Bob is blue. Bob is kind. Bob is red. Bob is rough. Bob is round. Bob is white. Kind people are red. Red people are rough. If Bob is blue and Bob is not kind then Bob is not big. If someone is rough and white then they are round. Kind people are round. White people are round. Kind people are big. If Bob is red then Bob is rough.
Bob is big.
("Bob" "is" "big" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is white.
("Bob" "is" "white" "+")
Kind people are red.
((("someone" "is" "kind" "+")) -> ("someone" "is" "red" "+"))
Red people are rough.
((("someone" "is" "red" "+")) -> ("someone" "is" "rough" "+"))
If Bob is blue and Bob is not kind then Bob is not big.
((("Bob" "is" "blue" "+") ("Bob" "is" "kind" "~")) -> ("Bob" "is" "big" "-"))
If someone is rough and white then they are round.
((("someone" "is" "rough" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "round" "+"))
Kind people are round.
((("someone" "is" "kind" "+")) -> ("someone" "is" "round" "+"))
White people are round.
((("someone" "is" "white" "+")) -> ("someone" "is" "round" "+"))
Kind people are big.
((("someone" "is" "kind" "+")) -> ("someone" "is" "big" "+"))
If Bob is red then Bob is rough.
((("Bob" "is" "red" "+")) -> ("Bob" "is" "rough" "+"))
Bob is white.
True
1
proof
[(triple7)]
("Bob" "is" "white" "+")
triple7
Bob is not blue.
False
1
inv-proof
[(triple2)]
("Bob" "is" "blue" "-")
triple2
@0: Bob is big.[(triple1 OR ((triple3) -> rule7))] Bob is blue.[(triple2)] Bob is kind.[(triple3)] Bob is red.[(triple4 OR ((triple3) -> rule1))] Bob is rough.[(triple5 OR ((triple4) -> rule2) OR ((triple4) -> rule8) OR ((((triple3) -> rule1)) -> rule2) OR ((((triple3) -> rule1)) -> rule8))] Bob is round.[(triple6 OR ((triple3) -> rule5) OR ((triple7) -> rule6) OR ((triple5 triple7) -> rule4) OR ((((triple4) -> rule2) triple7) -> rule4) OR ((((triple4) -> rule8) triple7) -> rule4) OR ((((((triple3) -> rule1)) -> rule2) triple7) -> rule4) OR ((((((triple3) -> rule1)) -> rule8) triple7) -> rule4))] Bob is white.[(triple7)]
Bob is big.
("Bob" "is" "big" "+")
triple1
((triple3) -> (rule7 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
triple2
Bob is kind.
("Bob" "is" "kind" "+")
triple3
Bob is red.
("Bob" "is" "red" "+")
triple4
((triple3) -> (rule1 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
triple5
((triple4) -> (rule2 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
((triple4) -> (rule8 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
((((triple3) -> (rule1 % int2))) -> (rule2 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
((((triple3) -> (rule1 % int2))) -> (rule8 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
triple6
((triple3) -> (rule5 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
((triple7) -> (rule6 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
((triple5 triple7) -> (rule4 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
((((triple4) -> (rule2 % int2)) triple7) -> (rule4 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
((((triple4) -> (rule8 % int2)) triple7) -> (rule4 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
((((((triple3) -> (rule1 % int3))) -> (rule2 % int2)) triple7) -> (rule4 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
((((((triple3) -> (rule1 % int3))) -> (rule8 % int2)) triple7) -> (rule4 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
Bob is white.
("Bob" "is" "white" "+")
triple7