Dave is big. Dave is cold. Dave is green. Dave is kind. Dave is nice. Dave is rough. Dave is young. Harry is big. Harry is cold. Harry is kind. Harry is rough. Harry is young. If something is young and kind then it is nice. If something is cold and young then it is green. If something is green and nice then it is big.
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 nice.
("Dave" "is" "nice" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is young.
("Dave" "is" "young" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is young.
("Harry" "is" "young" "+")
If something is young and kind then it is nice.
((("something" "is" "young" "+") ("something" "is" "kind" "+")) -> ("something" "is" "nice" "+"))
If something is cold and young then it is green.
((("something" "is" "cold" "+") ("something" "is" "young" "+")) -> ("something" "is" "green" "+"))
If something is green and nice then it is big.
((("something" "is" "green" "+") ("something" "is" "nice" "+")) -> ("something" "is" "big" "+"))
Dave is big.
True
1
proof
[(triple1 OR ((triple3 triple5) -> rule3) OR ((triple3 ((triple7 triple4) -> rule1)) -> rule3) OR ((((triple2 triple7) -> rule2) triple5) -> rule3) OR ((((triple2 triple7) -> rule2) ((triple7 triple4) -> rule1)) -> rule3))]
("Dave" "is" "big" "+")
triple1
((triple3 triple5) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
((triple3 ((triple7 triple4) -> (rule1 % int2))) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
((((triple2 triple7) -> (rule2 % int2)) triple5) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
((((triple2 triple7) -> (rule2 % int3)) ((triple7 triple4) -> (rule1 % int2))) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Harry is not rough.
False
1
inv-proof
[(triple11)]
("Harry" "is" "rough" "-")
triple11
Harry is green.
True
3
proof
[(((triple9 triple12) -> rule2))]
("Harry" "is" "green" "+")
((triple9 triple12) -> (rule2 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is not green.
False
3
inv-proof
[(((triple9 triple12) -> rule2))]
("Harry" "is" "green" "-")
((triple9 triple12) -> (rule2 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
@0: Dave is big.[(triple1 OR ((triple3 triple5) -> rule3) OR ((triple3 ((triple7 triple4) -> rule1)) -> rule3) OR ((((triple2 triple7) -> rule2) triple5) -> rule3) OR ((((triple2 triple7) -> rule2) ((triple7 triple4) -> rule1)) -> rule3))] Dave is cold.[(triple2)] Dave is green.[(triple3 OR ((triple2 triple7) -> rule2))] Dave is kind.[(triple4)] Dave is nice.[(triple5 OR ((triple7 triple4) -> rule1))] Dave is rough.[(triple6)] Dave is young.[(triple7)] Harry is big.[(triple8 OR ((((triple9 triple12) -> rule2) ((triple12 triple10) -> rule1)) -> rule3))] Harry is cold.[(triple9)] Harry is kind.[(triple10)] Harry is rough.[(triple11)] Harry is young.[(triple12)] @1: Harry is green.[(((triple9 triple12) -> rule2))] Harry is nice.[(((triple12 triple10) -> rule1))]
Dave is big.
("Dave" "is" "big" "+")
triple1
((triple3 triple5) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
((triple3 ((triple7 triple4) -> (rule1 % int2))) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
((((triple2 triple7) -> (rule2 % int2)) triple5) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
((((triple2 triple7) -> (rule2 % int3)) ((triple7 triple4) -> (rule1 % int2))) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Dave is cold.
("Dave" "is" "cold" "+")
triple2
Dave is green.
("Dave" "is" "green" "+")
triple3
((triple2 triple7) -> (rule2 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
triple4
Dave is nice.
("Dave" "is" "nice" "+")
triple5
((triple7 triple4) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
triple6
Dave is young.
("Dave" "is" "young" "+")
triple7
Harry is big.
("Harry" "is" "big" "+")
triple8
((((triple9 triple12) -> (rule2 % int3)) ((triple12 triple10) -> (rule1 % int2))) -> (rule3 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
Harry is cold.
("Harry" "is" "cold" "+")
triple9
Harry is kind.
("Harry" "is" "kind" "+")
triple10
Harry is rough.
("Harry" "is" "rough" "+")
triple11
Harry is young.
("Harry" "is" "young" "+")
triple12
Harry is green.
("Harry" "is" "green" "+")
((triple9 triple12) -> (rule2 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
((triple12 triple10) -> (rule1 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1