Bob is blue. Bob is kind. Bob is nice. Bob is rough. Bob is round. Bob is smart. Bob is young. Fiona is blue. Fiona is kind. Fiona is nice. Fiona is rough. Fiona is round. Fiona is smart. Fiona is not young. If Fiona is smart and Fiona is round then Fiona is not young. If someone is rough then they are nice. If someone is rough then they are kind.
Bob is blue.
("Bob" "is" "blue" "+")
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" "+")
Bob is young.
("Bob" "is" "young" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
Fiona is round.
("Fiona" "is" "round" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Fiona is not young.
("Fiona" "is" "young" "-")
If Fiona is smart and Fiona is round then Fiona is not young.
((("Fiona" "is" "smart" "+") ("Fiona" "is" "round" "+")) -> ("Fiona" "is" "young" "-"))
If someone is rough then they are nice.
((("someone" "is" "rough" "+")) -> ("someone" "is" "nice" "+"))
If someone is rough then they are kind.
((("someone" "is" "rough" "+")) -> ("someone" "is" "kind" "+"))
Bob is blue.
True
1
proof
[(triple1)]
("Bob" "is" "blue" "+")
triple1
Bob is not round.
False
1
inv-proof
[(triple5)]
("Bob" "is" "round" "-")
triple5
@0: Bob is blue.[(triple1)] Bob is kind.[(triple2 OR ((triple4) -> rule3))] Bob is nice.[(triple3 OR ((triple4) -> rule2))] Bob is rough.[(triple4)] Bob is round.[(triple5)] Bob is smart.[(triple6)] Bob is young.[(triple7)] Fiona is blue.[(triple8)] Fiona is kind.[(triple9 OR ((triple11) -> rule3))] Fiona is nice.[(triple10 OR ((triple11) -> rule2))] Fiona is not young.[(triple14 OR ((triple13 triple12) -> rule1))] Fiona is rough.[(triple11)] Fiona is round.[(triple12)] Fiona is smart.[(triple13)]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Bob is kind.
("Bob" "is" "kind" "+")
triple2
((triple4) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
triple3
((triple4) -> (rule2 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
triple4
Bob is round.
("Bob" "is" "round" "+")
triple5
Bob is smart.
("Bob" "is" "smart" "+")
triple6
Bob is young.
("Bob" "is" "young" "+")
triple7
Fiona is blue.
("Fiona" "is" "blue" "+")
triple8
Fiona is kind.
("Fiona" "is" "kind" "+")
triple9
((triple11) -> (rule3 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
triple10
((triple11) -> (rule2 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is not young.
("Fiona" "is" "young" "-")
triple14
((triple13 triple12) -> (rule1 % int1))
Fiona is not young.
("Fiona" "is" "young" "-")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
triple11
Fiona is round.
("Fiona" "is" "round" "+")
triple12
Fiona is smart.
("Fiona" "is" "smart" "+")
triple13