Charlie is blue. Charlie is green. Charlie is kind. Charlie is nice. Charlie is rough. Charlie is round. Charlie is young. Dave is blue. Dave is green. Dave is kind. Dave is nice. Dave is rough. Dave is round. Dave is young. All blue things are green. If Charlie is green then Charlie is round. Round things are rough.
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is young.
("Dave" "is" "young" "+")
All blue things are green.
((("something" "is" "blue" "+")) -> ("something" "is" "green" "+"))
If Charlie is green then Charlie is round.
((("Charlie" "is" "green" "+")) -> ("Charlie" "is" "round" "+"))
Round things are rough.
((("something" "is" "round" "+")) -> ("something" "is" "rough" "+"))
Charlie is rough.
True
1
proof
[(triple5 OR ((triple6) -> rule3) OR ((((triple2) -> rule2)) -> rule3) OR ((((((triple1) -> rule1)) -> rule2)) -> rule3))]
("Charlie" "is" "rough" "+")
triple5
((triple6) -> (rule3 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
((((triple2) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
((((((triple1) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
int3
Dave is not young.
False
1
inv-proof
[(triple14)]
("Dave" "is" "young" "-")
triple14
@0: Charlie is blue.[(triple1)] Charlie is green.[(triple2 OR ((triple1) -> rule1))] Charlie is kind.[(triple3)] Charlie is nice.[(triple4)] Charlie is rough.[(triple5 OR ((triple6) -> rule3) OR ((((triple2) -> rule2)) -> rule3) OR ((((((triple1) -> rule1)) -> rule2)) -> rule3))] Charlie is round.[(triple6 OR ((triple2) -> rule2) OR ((((triple1) -> rule1)) -> rule2))] Charlie is young.[(triple7)] Dave is blue.[(triple8)] Dave is green.[(triple9 OR ((triple8) -> rule1))] Dave is kind.[(triple10)] Dave is nice.[(triple11)] Dave is rough.[(triple12 OR ((triple13) -> rule3))] Dave is round.[(triple13)] Dave is young.[(triple14)]
Charlie is blue.
("Charlie" "is" "blue" "+")
triple1
Charlie is green.
("Charlie" "is" "green" "+")
triple2
((triple1) -> (rule1 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
triple3
Charlie is nice.
("Charlie" "is" "nice" "+")
triple4
Charlie is rough.
("Charlie" "is" "rough" "+")
triple5
((triple6) -> (rule3 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
((((triple2) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
((((((triple1) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
int3
Charlie is round.
("Charlie" "is" "round" "+")
triple6
((triple2) -> (rule2 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
triple7
Dave is blue.
("Dave" "is" "blue" "+")
triple8
Dave is green.
("Dave" "is" "green" "+")
triple9
((triple8) -> (rule1 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
triple10
Dave is nice.
("Dave" "is" "nice" "+")
triple11
Dave is rough.
("Dave" "is" "rough" "+")
triple12
((triple13) -> (rule3 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
triple13
Dave is young.
("Dave" "is" "young" "+")
triple14