Bob is big. Bob is blue. Bob is quiet. Bob is rough. Bob is round. Bob is smart. Bob is young. If Bob is quiet and Bob is round then Bob is young. If something is smart and quiet then it is big. Round, smart things are young.
Bob is big.
("Bob" "is" "big" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Bob is young.
("Bob" "is" "young" "+")
If Bob is quiet and Bob is round then Bob is young.
((("Bob" "is" "quiet" "+") ("Bob" "is" "round" "+")) -> ("Bob" "is" "young" "+"))
If something is smart and quiet then it is big.
((("something" "is" "smart" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "big" "+"))
Round, smart things are young.
((("something" "is" "round" "+") ("something" "is" "smart" "+")) -> ("something" "is" "young" "+"))
Bob is young.
True
1
proof
[(triple7 OR ((triple3 triple5) -> rule1) OR ((triple5 triple6) -> rule3))]
("Bob" "is" "young" "+")
triple7
((triple3 triple5) -> (rule1 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
((triple5 triple6) -> (rule3 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is not young.
False
1
inv-proof
[(triple7 OR ((triple3 triple5) -> rule1) OR ((triple5 triple6) -> rule3))]
("Bob" "is" "young" "-")
triple7
((triple3 triple5) -> (rule1 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
((triple5 triple6) -> (rule3 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
@0: Bob is big.[(triple1 OR ((triple6 triple3) -> rule2))] Bob is blue.[(triple2)] Bob is quiet.[(triple3)] Bob is rough.[(triple4)] Bob is round.[(triple5)] Bob is smart.[(triple6)] Bob is young.[(triple7 OR ((triple3 triple5) -> rule1) OR ((triple5 triple6) -> rule3))]
Bob is big.
("Bob" "is" "big" "+")
triple1
((triple6 triple3) -> (rule2 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
triple2
Bob is quiet.
("Bob" "is" "quiet" "+")
triple3
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
((triple3 triple5) -> (rule1 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
((triple5 triple6) -> (rule3 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1