Bob is big. Bob is nice. Bob is quiet. Bob is rough. Bob is round. Bob is smart. Bob is white. Charlie is big. Charlie is nice. Charlie is round. Charlie is smart. Gary is nice. Gary is quiet. Gary is round. Gary is smart. Gary is white. If something is quiet and smart then it is white. All smart things are quiet. If something is quiet then it is rough.
Bob is big.
("Bob" "is" "big" "+")
Bob is nice.
("Bob" "is" "nice" "+")
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 white.
("Bob" "is" "white" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is round.
("Gary" "is" "round" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Gary is white.
("Gary" "is" "white" "+")
If something is quiet and smart then it is white.
((("something" "is" "quiet" "+") ("something" "is" "smart" "+")) -> ("something" "is" "white" "+"))
All smart things are quiet.
((("something" "is" "smart" "+")) -> ("something" "is" "quiet" "+"))
If something is quiet then it is rough.
((("something" "is" "quiet" "+")) -> ("something" "is" "rough" "+"))
Bob is big.
True
1
proof
[(triple1)]
("Bob" "is" "big" "+")
triple1
Bob is not white.
False
1
inv-proof
[(triple7 OR ((triple3 triple6) -> rule1) OR ((((triple6) -> rule2) triple6) -> rule1))]
("Bob" "is" "white" "-")
triple7
((triple3 triple6) -> (rule1 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
((((triple6) -> (rule2 % int2)) triple6) -> (rule1 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Gary is rough.
True
2
proof
[(((triple13) -> rule3) OR ((((triple15) -> rule2)) -> rule3))]
("Gary" "is" "rough" "+")
((triple13) -> (rule3 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
((((triple15) -> (rule2 % int2))) -> (rule3 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Charlie is not quiet.
False
2
inv-proof
[(((triple11) -> rule2))]
("Charlie" "is" "quiet" "-")
((triple11) -> (rule2 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is rough.
True
3
proof
[(((((triple11) -> rule2)) -> rule3))]
("Charlie" "is" "rough" "+")
((((triple11) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is not white.
False
4
inv-proof
[(((((triple11) -> rule2) triple11) -> rule1))]
("Charlie" "is" "white" "-")
((((triple11) -> (rule2 % int2)) triple11) -> (rule1 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
@0: Bob is big.[(triple1)] Bob is nice.[(triple2)] Bob is quiet.[(triple3 OR ((triple6) -> rule2))] Bob is rough.[(triple4 OR ((triple3) -> rule3) OR ((((triple6) -> rule2)) -> rule3))] Bob is round.[(triple5)] Bob is smart.[(triple6)] Bob is white.[(triple7 OR ((triple3 triple6) -> rule1) OR ((((triple6) -> rule2) triple6) -> rule1))] Charlie is big.[(triple8)] Charlie is nice.[(triple9)] Charlie is round.[(triple10)] Charlie is smart.[(triple11)] Gary is nice.[(triple12)] Gary is quiet.[(triple13 OR ((triple15) -> rule2))] Gary is round.[(triple14)] Gary is smart.[(triple15)] Gary is white.[(triple16 OR ((triple13 triple15) -> rule1) OR ((((triple15) -> rule2) triple15) -> rule1))] @1: Charlie is quiet.[(((triple11) -> rule2))] Gary is rough.[(((triple13) -> rule3) OR ((((triple15) -> rule2)) -> rule3))] @2: Charlie is rough.[(((((triple11) -> rule2)) -> rule3))] Charlie is white.[(((((triple11) -> rule2) triple11) -> rule1))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is nice.
("Bob" "is" "nice" "+")
triple2
Bob is quiet.
("Bob" "is" "quiet" "+")
triple3
((triple6) -> (rule2 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
triple4
((triple3) -> (rule3 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
((((triple6) -> (rule2 % int2))) -> (rule3 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
triple5
Bob is smart.
("Bob" "is" "smart" "+")
triple6
Bob is white.
("Bob" "is" "white" "+")
triple7
((triple3 triple6) -> (rule1 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
((((triple6) -> (rule2 % int2)) triple6) -> (rule1 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
triple8
Charlie is nice.
("Charlie" "is" "nice" "+")
triple9
Charlie is round.
("Charlie" "is" "round" "+")
triple10
Charlie is smart.
("Charlie" "is" "smart" "+")
triple11
Gary is nice.
("Gary" "is" "nice" "+")
triple12
Gary is quiet.
("Gary" "is" "quiet" "+")
triple13
((triple15) -> (rule2 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
triple14
Gary is smart.
("Gary" "is" "smart" "+")
triple15
Gary is white.
("Gary" "is" "white" "+")
triple16
((triple13 triple15) -> (rule1 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
((((triple15) -> (rule2 % int2)) triple15) -> (rule1 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((triple11) -> (rule2 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
((triple13) -> (rule3 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
((((triple15) -> (rule2 % int2))) -> (rule3 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
((((triple11) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
((((triple11) -> (rule2 % int2)) triple11) -> (rule1 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2