Charlie is green. Charlie is quiet. Charlie is smart. Charlie is white. Charlie is young. Dave is green. Dave is kind. Dave is nice. Dave is quiet. Dave is smart. Dave is white. Dave is young. All nice things are green. If Charlie is white and Charlie is young then Charlie is smart. Smart things are kind.
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is white.
("Dave" "is" "white" "+")
Dave is young.
("Dave" "is" "young" "+")
All nice things are green.
((("something" "is" "nice" "+")) -> ("something" "is" "green" "+"))
If Charlie is white and Charlie is young then Charlie is smart.
((("Charlie" "is" "white" "+") ("Charlie" "is" "young" "+")) -> ("Charlie" "is" "smart" "+"))
Smart things are kind.
((("something" "is" "smart" "+")) -> ("something" "is" "kind" "+"))
Charlie is white.
True
1
proof
[(triple4)]
("Charlie" "is" "white" "+")
triple4
Charlie is not quiet.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "quiet" "-")
triple2
Charlie is kind.
True
2
proof
[(((triple3) -> rule3) OR ((((triple4 triple5) -> rule2)) -> rule3))]
("Charlie" "is" "kind" "+")
((triple3) -> (rule3 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
((((triple4 triple5) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is not kind.
False
2
inv-proof
[(((triple3) -> rule3) OR ((((triple4 triple5) -> rule2)) -> rule3))]
("Charlie" "is" "kind" "-")
((triple3) -> (rule3 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
((((triple4 triple5) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
@0: Charlie is green.[(triple1)] Charlie is quiet.[(triple2)] Charlie is smart.[(triple3 OR ((triple4 triple5) -> rule2))] Charlie is white.[(triple4)] Charlie is young.[(triple5)] Dave is green.[(triple6 OR ((triple8) -> rule1))] Dave is kind.[(triple7 OR ((triple10) -> rule3))] Dave is nice.[(triple8)] Dave is quiet.[(triple9)] Dave is smart.[(triple10)] Dave is white.[(triple11)] Dave is young.[(triple12)] @1: Charlie is kind.[(((triple3) -> rule3) OR ((((triple4 triple5) -> rule2)) -> rule3))]
Charlie is green.
("Charlie" "is" "green" "+")
triple1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple2
Charlie is smart.
("Charlie" "is" "smart" "+")
triple3
((triple4 triple5) -> (rule2 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
triple4
Charlie is young.
("Charlie" "is" "young" "+")
triple5
Dave is green.
("Dave" "is" "green" "+")
triple6
((triple8) -> (rule1 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
triple7
((triple10) -> (rule3 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
triple8
Dave is quiet.
("Dave" "is" "quiet" "+")
triple9
Dave is smart.
("Dave" "is" "smart" "+")
triple10
Dave is white.
("Dave" "is" "white" "+")
triple11
Dave is young.
("Dave" "is" "young" "+")
triple12
Charlie is kind.
("Charlie" "is" "kind" "+")
((triple3) -> (rule3 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
((((triple4 triple5) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2