Charlie is big. Charlie is cold. Charlie is green. Charlie is nice. Charlie is rough. Charlie is white. Charlie is young. Dave is big. Dave is cold. Dave is green. Dave is white. Dave is young. If someone is green then they are rough.
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is white.
("Dave" "is" "white" "+")
Dave is young.
("Dave" "is" "young" "+")
If someone is green then they are rough.
((("someone" "is" "green" "+")) -> ("someone" "is" "rough" "+"))
Charlie is green.
True
1
proof
[(triple3)]
("Charlie" "is" "green" "+")
triple3
Charlie is not cold.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "cold" "-")
triple2
Dave is rough.
True
2
proof
[(((triple10) -> rule1))]
("Dave" "is" "rough" "+")
((triple10) -> (rule1 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is not rough.
False
2
inv-proof
[(((triple10) -> rule1))]
("Dave" "is" "rough" "-")
((triple10) -> (rule1 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
@0: Charlie is big.[(triple1)] Charlie is cold.[(triple2)] Charlie is green.[(triple3)] Charlie is nice.[(triple4)] Charlie is rough.[(triple5 OR ((triple3) -> rule1))] Charlie is white.[(triple6)] Charlie is young.[(triple7)] Dave is big.[(triple8)] Dave is cold.[(triple9)] Dave is green.[(triple10)] Dave is white.[(triple11)] Dave is young.[(triple12)] @1: Dave is rough.[(((triple10) -> rule1))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
Charlie is cold.
("Charlie" "is" "cold" "+")
triple2
Charlie is green.
("Charlie" "is" "green" "+")
triple3
Charlie is nice.
("Charlie" "is" "nice" "+")
triple4
Charlie is rough.
("Charlie" "is" "rough" "+")
triple5
((triple3) -> (rule1 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
triple6
Charlie is young.
("Charlie" "is" "young" "+")
triple7
Dave is big.
("Dave" "is" "big" "+")
triple8
Dave is cold.
("Dave" "is" "cold" "+")
triple9
Dave is green.
("Dave" "is" "green" "+")
triple10
Dave is white.
("Dave" "is" "white" "+")
triple11
Dave is young.
("Dave" "is" "young" "+")
triple12
Dave is rough.
("Dave" "is" "rough" "+")
((triple10) -> (rule1 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1