Bob is big. Bob is green. Bob is red. Bob is rough. Bob is young. Charlie is big. Charlie is furry. Charlie is green. Charlie is red. Charlie is rough. Charlie is smart. Charlie is young. If something is furry then it is smart. If Bob is furry and Bob is young then Bob is red. Red, green things are furry.
Bob is big.
("Bob" "is" "big" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is young.
("Bob" "is" "young" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Charlie is young.
("Charlie" "is" "young" "+")
If something is furry then it is smart.
((("something" "is" "furry" "+")) -> ("something" "is" "smart" "+"))
If Bob is furry and Bob is young then Bob is red.
((("Bob" "is" "furry" "+") ("Bob" "is" "young" "+")) -> ("Bob" "is" "red" "+"))
Red, green things are furry.
((("something" "is" "red" "+") ("something" "is" "green" "+")) -> ("something" "is" "furry" "+"))
Charlie is young.
True
1
proof
[(triple12)]
("Charlie" "is" "young" "+")
triple12
Bob is not big.
False
1
inv-proof
[(triple1)]
("Bob" "is" "big" "-")
triple1
Bob is furry.
True
3
proof
[(((triple3 triple2) -> rule3))]
("Bob" "is" "furry" "+")
((triple3 triple2) -> (rule3 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is not furry.
False
3
inv-proof
[(((triple3 triple2) -> rule3))]
("Bob" "is" "furry" "-")
((triple3 triple2) -> (rule3 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is smart.
True
4
proof
[(((((triple3 triple2) -> rule3)) -> rule1))]
("Bob" "is" "smart" "+")
((((triple3 triple2) -> (rule3 % int2))) -> (rule1 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is not smart.
False
4
inv-proof
[(((((triple3 triple2) -> rule3)) -> rule1))]
("Bob" "is" "smart" "-")
((((triple3 triple2) -> (rule3 % int2))) -> (rule1 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
@0: Bob is big.[(triple1)] Bob is green.[(triple2)] Bob is red.[(triple3)] Bob is rough.[(triple4)] Bob is young.[(triple5)] Charlie is big.[(triple6)] Charlie is furry.[(triple7 OR ((triple9 triple8) -> rule3))] Charlie is green.[(triple8)] Charlie is red.[(triple9)] Charlie is rough.[(triple10)] Charlie is smart.[(triple11 OR ((triple7) -> rule1) OR ((((triple9 triple8) -> rule3)) -> rule1))] Charlie is young.[(triple12)] @1: Bob is furry.[(((triple3 triple2) -> rule3))] @2: Bob is smart.[(((((triple3 triple2) -> rule3)) -> rule1))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is green.
("Bob" "is" "green" "+")
triple2
Bob is red.
("Bob" "is" "red" "+")
triple3
Bob is rough.
("Bob" "is" "rough" "+")
triple4
Bob is young.
("Bob" "is" "young" "+")
triple5
Charlie is big.
("Charlie" "is" "big" "+")
triple6
Charlie is furry.
("Charlie" "is" "furry" "+")
triple7
((triple9 triple8) -> (rule3 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
triple8
Charlie is red.
("Charlie" "is" "red" "+")
triple9
Charlie is rough.
("Charlie" "is" "rough" "+")
triple10
Charlie is smart.
("Charlie" "is" "smart" "+")
triple11
((triple7) -> (rule1 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
((((triple9 triple8) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
triple12
Bob is furry.
("Bob" "is" "furry" "+")
((triple3 triple2) -> (rule3 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
((((triple3 triple2) -> (rule3 % int2))) -> (rule1 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2