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