Charlie is blue. Charlie is green. Charlie is kind. Charlie is nice. Charlie is red. Charlie is smart. Charlie is young. Dave is blue. Dave is green. Dave is kind. Dave is nice. Dave is smart. All kind, young things are red. If something is smart then it is young.
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 red.
("Charlie" "is" "red" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
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 smart.
("Dave" "is" "smart" "+")
All kind, young things are red.
((("something" "is" "kind" "+") ("something" "is" "young" "+")) -> ("something" "is" "red" "+"))
If something is smart then it is young.
((("something" "is" "smart" "+")) -> ("something" "is" "young" "+"))
Charlie is green.
True
1
proof
[(triple2)]
("Charlie" "is" "green" "+")
triple2
Dave is not blue.
False
1
inv-proof
[(triple8)]
("Dave" "is" "blue" "-")
triple8
Dave is young.
True
2
proof
[(((triple12) -> rule2))]
("Dave" "is" "young" "+")
((triple12) -> (rule2 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is not young.
False
2
inv-proof
[(((triple12) -> rule2))]
("Dave" "is" "young" "-")
((triple12) -> (rule2 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is red.
True
4
proof
[(((triple10 ((triple12) -> rule2)) -> rule1))]
("Dave" "is" "red" "+")
((triple10 ((triple12) -> (rule2 % int2))) -> (rule1 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is not red.
False
4
inv-proof
[(((triple10 ((triple12) -> rule2)) -> rule1))]
("Dave" "is" "red" "-")
((triple10 ((triple12) -> (rule2 % int2))) -> (rule1 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
@0: Charlie is blue.[(triple1)] Charlie is green.[(triple2)] Charlie is kind.[(triple3)] Charlie is nice.[(triple4)] Charlie is red.[(triple5 OR ((triple3 triple7) -> rule1) OR ((triple3 ((triple6) -> rule2)) -> rule1))] Charlie is smart.[(triple6)] Charlie is young.[(triple7 OR ((triple6) -> rule2))] Dave is blue.[(triple8)] Dave is green.[(triple9)] Dave is kind.[(triple10)] Dave is nice.[(triple11)] Dave is smart.[(triple12)] @1: Dave is young.[(((triple12) -> rule2))] @2: Dave is red.[(((triple10 ((triple12) -> rule2)) -> rule1))]
Charlie is blue.
("Charlie" "is" "blue" "+")
triple1
Charlie is green.
("Charlie" "is" "green" "+")
triple2
Charlie is kind.
("Charlie" "is" "kind" "+")
triple3
Charlie is nice.
("Charlie" "is" "nice" "+")
triple4
Charlie is red.
("Charlie" "is" "red" "+")
triple5
((triple3 triple7) -> (rule1 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
((triple3 ((triple6) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
triple6
Charlie is young.
("Charlie" "is" "young" "+")
triple7
((triple6) -> (rule2 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
triple8
Dave is green.
("Dave" "is" "green" "+")
triple9
Dave is kind.
("Dave" "is" "kind" "+")
triple10
Dave is nice.
("Dave" "is" "nice" "+")
triple11
Dave is smart.
("Dave" "is" "smart" "+")
triple12
Dave is young.
("Dave" "is" "young" "+")
((triple12) -> (rule2 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
((triple10 ((triple12) -> (rule2 % int2))) -> (rule1 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2