Bob is big. Bob is green. Bob is nice. All red, smart things are not big. Big things are nice. If something is smart then it is not rough. If something is smart then it is green. Big, green things are smart. If something is green and not rough then it is quiet.
Bob is big.
("Bob" "is" "big" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is nice.
("Bob" "is" "nice" "+")
All red, smart things are not big.
((("something" "is" "red" "+") ("something" "is" "smart" "+")) -> ("something" "is" "big" "-"))
Big things are nice.
((("something" "is" "big" "+")) -> ("something" "is" "nice" "+"))
If something is smart then it is not rough.
((("something" "is" "smart" "+")) -> ("something" "is" "rough" "-"))
If something is smart then it is green.
((("something" "is" "smart" "+")) -> ("something" "is" "green" "+"))
Big, green things are smart.
((("something" "is" "big" "+") ("something" "is" "green" "+")) -> ("something" "is" "smart" "+"))
If something is green and not rough then it is quiet.
((("something" "is" "green" "+") ("something" "is" "rough" "~")) -> ("something" "is" "quiet" "+"))
Bob is nice.
True
1
proof
[(triple3 OR ((triple1) -> rule2))]
("Bob" "is" "nice" "+")
triple3
((triple1) -> (rule2 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is not big.
False
1
inv-proof
[(triple1)]
("Bob" "is" "big" "-")
triple1
Bob is smart.
True
3
proof
[(((triple1 triple2) -> rule5))]
("Bob" "is" "smart" "+")
((triple1 triple2) -> (rule5 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is not smart.
False
3
inv-proof
[(((triple1 triple2) -> rule5))]
("Bob" "is" "smart" "-")
((triple1 triple2) -> (rule5 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is not rough.
True
4
proof
[(((((triple1 triple2) -> rule5)) -> rule3))]
("Bob" "is" "rough" "-")
((((triple1 triple2) -> (rule5 % int2))) -> (rule3 % int1))
Bob is not rough.
("Bob" "is" "rough" "-")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is rough.
False
4
inv-proof
[(((((triple1 triple2) -> rule5)) -> rule3))]
("Bob" "is" "rough" "+")
((((triple1 triple2) -> (rule5 % int2))) -> (rule3 % int1))
Bob is not rough.
("Bob" "is" "rough" "-")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
@0: Bob is big.[(triple1)] Bob is green.[(triple2)] Bob is nice.[(triple3 OR ((triple1) -> rule2))] @1: Bob is smart.[(((triple1 triple2) -> rule5))] @2: Bob is not rough.[(((((triple1 triple2) -> rule5)) -> rule3))] @3: Bob is quiet.[(((triple2 ((((triple1 triple2) -> rule5)) -> rule3)) -> rule6))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is green.
("Bob" "is" "green" "+")
triple2
Bob is nice.
("Bob" "is" "nice" "+")
triple3
((triple1) -> (rule2 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
((triple1 triple2) -> (rule5 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is not rough.
("Bob" "is" "rough" "-")
((((triple1 triple2) -> (rule5 % int2))) -> (rule3 % int1))
Bob is not rough.
("Bob" "is" "rough" "-")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
((triple2 ((((triple1 triple2) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is not rough.
("Bob" "is" "rough" "-")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3