Anne is nice. Anne is quiet. Anne is red. Anne is rough. Anne is young. Bob is big. Bob is nice. Bob is quiet. Bob is red. Bob is not rough. Bob is round. Bob is young. If something is rough then it is big. If something is nice and not red then it is rough. If something is young and big then it is round.
Anne is nice.
("Anne" "is" "nice" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is young.
("Anne" "is" "young" "+")
Bob is big.
("Bob" "is" "big" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is not rough.
("Bob" "is" "rough" "-")
Bob is round.
("Bob" "is" "round" "+")
Bob is young.
("Bob" "is" "young" "+")
If something is rough then it is big.
((("something" "is" "rough" "+")) -> ("something" "is" "big" "+"))
If something is nice and not red then it is rough.
((("something" "is" "nice" "+") ("something" "is" "red" "~")) -> ("something" "is" "rough" "+"))
If something is young and big then it is round.
((("something" "is" "young" "+") ("something" "is" "big" "+")) -> ("something" "is" "round" "+"))
Bob is red.
True
1
proof
[(triple9)]
("Bob" "is" "red" "+")
triple9
Bob is rough.
False
1
inv-proof
[(triple10)]
("Bob" "is" "rough" "+")
triple10
Anne is big.
True
2
proof
[(((triple4) -> rule1))]
("Anne" "is" "big" "+")
((triple4) -> (rule1 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is not big.
False
2
inv-proof
[(((triple4) -> rule1))]
("Anne" "is" "big" "-")
((triple4) -> (rule1 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is round.
True
4
proof
[(((triple5 ((triple4) -> rule1)) -> rule3))]
("Anne" "is" "round" "+")
((triple5 ((triple4) -> (rule1 % int2))) -> (rule3 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is not round.
False
4
inv-proof
[(((triple5 ((triple4) -> rule1)) -> rule3))]
("Anne" "is" "round" "-")
((triple5 ((triple4) -> (rule1 % int2))) -> (rule3 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
@0: Anne is nice.[(triple1)] Anne is quiet.[(triple2)] Anne is red.[(triple3)] Anne is rough.[(triple4)] Anne is young.[(triple5)] Bob is big.[(triple6)] Bob is nice.[(triple7)] Bob is not rough.[(triple10)] Bob is quiet.[(triple8)] Bob is red.[(triple9)] Bob is round.[(triple11 OR ((triple12 triple6) -> rule3))] Bob is young.[(triple12)] @1: Anne is big.[(((triple4) -> rule1))] @2: Anne is round.[(((triple5 ((triple4) -> rule1)) -> rule3))]
Anne is nice.
("Anne" "is" "nice" "+")
triple1
Anne is quiet.
("Anne" "is" "quiet" "+")
triple2
Anne is red.
("Anne" "is" "red" "+")
triple3
Anne is rough.
("Anne" "is" "rough" "+")
triple4
Anne is young.
("Anne" "is" "young" "+")
triple5
Bob is big.
("Bob" "is" "big" "+")
triple6
Bob is nice.
("Bob" "is" "nice" "+")
triple7
Bob is not rough.
("Bob" "is" "rough" "-")
triple10
Bob is quiet.
("Bob" "is" "quiet" "+")
triple8
Bob is red.
("Bob" "is" "red" "+")
triple9
Bob is round.
("Bob" "is" "round" "+")
triple11
((triple12 triple6) -> (rule3 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
triple12
Anne is big.
("Anne" "is" "big" "+")
((triple4) -> (rule1 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
((triple5 ((triple4) -> (rule1 % int2))) -> (rule3 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2