Bob is big. Bob is blue. Bob is cold. Bob is furry. Bob is smart. Charlie is big. Charlie is blue. Charlie is cold. Charlie is furry. Charlie is rough. Charlie is smart. Charlie is white. All big people are rough.
Bob is big.
("Bob" "is" "big" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Charlie is white.
("Charlie" "is" "white" "+")
All big people are rough.
((("someone" "is" "big" "+")) -> ("someone" "is" "rough" "+"))
Charlie is white.
True
1
proof
[(triple12)]
("Charlie" "is" "white" "+")
triple12
Bob is not big.
False
1
inv-proof
[(triple1)]
("Bob" "is" "big" "-")
triple1
Bob is rough.
True
2
proof
[(((triple1) -> rule1))]
("Bob" "is" "rough" "+")
((triple1) -> (rule1 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is not rough.
False
2
inv-proof
[(((triple1) -> rule1))]
("Bob" "is" "rough" "-")
((triple1) -> (rule1 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
@0: Bob is big.[(triple1)] Bob is blue.[(triple2)] Bob is cold.[(triple3)] Bob is furry.[(triple4)] Bob is smart.[(triple5)] Charlie is big.[(triple6)] Charlie is blue.[(triple7)] Charlie is cold.[(triple8)] Charlie is furry.[(triple9)] Charlie is rough.[(triple10 OR ((triple6) -> rule1))] Charlie is smart.[(triple11)] Charlie is white.[(triple12)] @1: Bob is rough.[(((triple1) -> rule1))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is blue.
("Bob" "is" "blue" "+")
triple2
Bob is cold.
("Bob" "is" "cold" "+")
triple3
Bob is furry.
("Bob" "is" "furry" "+")
triple4
Bob is smart.
("Bob" "is" "smart" "+")
triple5
Charlie is big.
("Charlie" "is" "big" "+")
triple6
Charlie is blue.
("Charlie" "is" "blue" "+")
triple7
Charlie is cold.
("Charlie" "is" "cold" "+")
triple8
Charlie is furry.
("Charlie" "is" "furry" "+")
triple9
Charlie is rough.
("Charlie" "is" "rough" "+")
triple10
((triple6) -> (rule1 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
triple11
Charlie is white.
("Charlie" "is" "white" "+")
triple12
Bob is rough.
("Bob" "is" "rough" "+")
((triple1) -> (rule1 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1